Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimpcd | Unicode version |
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Ref | Expression |
---|---|
biimpcd.1 |
Ref | Expression |
---|---|
biimpcd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | biimpcd.1 | . 2 | |
3 | 1, 2 | syl5ibcom 154 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpac 296 3impexpbicom 1425 ax16 1800 ax16i 1845 nelneq 2265 nelneq2 2266 nelne1 2424 nelne2 2425 spc2gv 2812 spc3gv 2814 nssne1 3195 nssne2 3196 ifbothdc 3547 difsn 3704 iununir 3943 nbrne1 3995 nbrne2 3996 ss1o0el1 4170 mosubopt 4663 issref 4980 ssimaex 5541 chfnrn 5590 ffnfv 5637 f1elima 5735 dftpos4 6222 tfr1onlemsucaccv 6300 tfrcllemsucaccv 6313 snon0 6892 exmidonfinlem 7140 enq0sym 7364 prop 7407 prubl 7418 negf1o 8271 0fz1 9970 elfzmlbp 10057 maxleast 11141 negfi 11155 isprm2 12028 nprmdvds1 12051 oddprmdvds 12263 exmidsbthrlem 13742 |
Copyright terms: Public domain | W3C validator |