![]() |
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 153 | 1 ⊢ (𝜓 → (𝜑 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: biimpac 292 3impexpbicom 1368 ax16 1735 ax16i 1780 nelneq 2180 nelneq2 2181 nelne1 2336 nelne2 2337 spc2gv 2689 spc3gv 2691 nssne1 3056 nssne2 3057 ifbothdc 3382 difsn 3525 iununir 3761 nbrne1 3804 nbrne2 3805 mosubopt 4425 issref 4731 ssimaex 5260 chfnrn 5304 ffnfv 5349 f1elima 5438 dftpos4 5906 tfr1onlemsucaccv 5984 tfrcllemsucaccv 5997 snon0 6435 enq0sym 6673 prop 6716 prubl 6727 negf1o 7542 0fz1 9129 elfzmlbp 9209 maxleast 10226 negfi 10237 isprm2 10632 nprmdvds1 10654 |
Copyright terms: Public domain | W3C validator |