Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impbid1 | GIF version |
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
Ref | Expression |
---|---|
impbid1.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
impbid1.2 | ⊢ (𝜒 → 𝜓) |
Ref | Expression |
---|---|
impbid1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbid1.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | impbid1.2 | . . 3 ⊢ (𝜒 → 𝜓) | |
3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | impbid 128 | 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-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: impbid2 142 iba 298 ibar 299 pm4.81dc 893 pm5.63dc 930 pm4.83dc 935 pm5.71dc 945 19.33b2 1608 19.9t 1621 sb4b 1806 a16gb 1837 euor2 2057 eupickbi 2081 ceqsalg 2714 eqvincg 2809 ddifstab 3208 csbprc 3408 undif4 3425 eqifdc 3506 sssnm 3681 sneqbg 3690 opthpr 3699 elpwuni 3902 exmid01 4121 exmidundif 4129 eusv2i 4376 reusv3 4381 iunpw 4401 suc11g 4472 ssxpbm 4974 ssxp1 4975 ssxp2 4976 xp11m 4977 2elresin 5234 mpteqb 5511 f1fveq 5673 f1elima 5674 f1imass 5675 fliftf 5700 nnsucuniel 6391 iserd 6455 ecopovtrn 6526 ecopover 6527 ecopovtrng 6529 ecopoverg 6530 map0g 6582 fopwdom 6730 f1finf1o 6835 mkvprop 7032 addcanpig 7142 mulcanpig 7143 srpospr 7591 readdcan 7902 cnegexlem1 7937 addcan 7942 addcan2 7943 neg11 8013 negreb 8027 add20 8236 cru 8364 mulcanapd 8422 uz11 9348 eqreznegel 9406 lbzbi 9408 xneg11 9617 xnn0xadd0 9650 xsubge0 9664 elioc2 9719 elico2 9720 elicc2 9721 fzopth 9841 2ffzeq 9918 flqidz 10059 addmodlteq 10171 frec2uzrand 10178 expcan 10463 nn0opthd 10468 fz1eqb 10537 cj11 10677 sqrt0 10776 recan 10881 0dvds 11513 dvds1 11551 alzdvds 11552 nn0enne 11599 nn0oddm1d2 11606 nnoddm1d2 11607 divalgmod 11624 gcdeq0 11665 algcvgblem 11730 prmexpb 11829 ennnfonelemim 11937 tgdom 12241 en1top 12246 hmeocnvb 12487 metrest 12675 bj-nnbist 12953 bj-nnbidc 12962 bj-peano4 13153 bj-nn0sucALT 13176 |
Copyright terms: Public domain | W3C validator |