Description: A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | biimpexp | |- ( ( ( ph <-> ps ) -> ch ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi2 | |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) |
|
2 | 1 | imbi1i | |- ( ( ( ph <-> ps ) -> ch ) <-> ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ch ) ) |
3 | impexp | |- ( ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ch ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> ch ) ) ) |
|
4 | 2 3 | bitri | |- ( ( ( ph <-> ps ) -> ch ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> ch ) ) ) |