Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.32d | Unicode version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm5.32d.1 |
Ref | Expression |
---|---|
pm5.32d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32d.1 | . . . 4 | |
2 | biimp 117 | . . . 4 | |
3 | 1, 2 | syl6 33 | . . 3 |
4 | 3 | imdistand 445 | . 2 |
5 | biimpr 129 | . . . 4 | |
6 | 1, 5 | syl6 33 | . . 3 |
7 | 6 | imdistand 445 | . 2 |
8 | 4, 7 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.32rd 448 pm5.32da 449 pm5.32 450 anbi2d 461 cbvex2 1915 cores 5114 isoini 5797 mpoeq123 5912 genpassl 7486 genpassu 7487 fzind 9327 btwnz 9331 elfzm11 10047 isprm2 12071 isprm3 12072 modprminv 12203 modprminveq 12204 |
Copyright terms: Public domain | W3C validator |