Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimpcd | GIF 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 1414 ax16 1785 ax16i 1830 nelneq 2240 nelneq2 2241 nelne1 2398 nelne2 2399 spc2gv 2776 spc3gv 2778 nssne1 3155 nssne2 3156 ifbothdc 3504 difsn 3657 iununir 3896 nbrne1 3947 nbrne2 3948 exmid01 4121 mosubopt 4604 issref 4921 ssimaex 5482 chfnrn 5531 ffnfv 5578 f1elima 5674 dftpos4 6160 tfr1onlemsucaccv 6238 tfrcllemsucaccv 6251 snon0 6824 exmidonfinlem 7049 enq0sym 7240 prop 7283 prubl 7294 negf1o 8144 0fz1 9825 elfzmlbp 9909 maxleast 10985 negfi 10999 isprm2 11798 nprmdvds1 11820 exmidsbthrlem 13217 |
Copyright terms: Public domain | W3C validator |