![]() |
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 129 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: impbid2 143 iba 300 ibar 301 pm4.81dc 908 pm5.63dc 946 pm4.83dc 951 pm5.71dc 961 19.33b2 1629 19.9t 1642 sb4b 1834 a16gb 1865 euor2 2084 eupickbi 2108 ceqsalg 2765 eqvincg 2861 ddifstab 3267 csbprc 3468 undif4 3485 eqifdc 3569 sssnm 3754 sneqbg 3763 opthpr 3772 elpwuni 3975 ss1o0el1 4196 exmid01 4197 exmidundif 4205 eusv2i 4454 reusv3 4459 iunpw 4479 suc11g 4555 ssxpbm 5063 ssxp1 5064 ssxp2 5065 xp11m 5066 2elresin 5326 mpteqb 5605 f1fveq 5770 f1elima 5771 f1imass 5772 fliftf 5797 nnsucuniel 6493 iserd 6558 ecopovtrn 6629 ecopover 6630 ecopovtrng 6632 ecopoverg 6633 map0g 6685 fopwdom 6833 f1finf1o 6943 mkvprop 7153 addcanpig 7330 mulcanpig 7331 srpospr 7779 readdcan 8093 cnegexlem1 8128 addcan 8133 addcan2 8134 neg11 8204 negreb 8218 add20 8427 cru 8555 mulcanapd 8614 uz11 9546 eqreznegel 9610 lbzbi 9612 xneg11 9830 xnn0xadd0 9863 xsubge0 9877 elioc2 9932 elico2 9933 elicc2 9934 fzopth 10056 2ffzeq 10136 flqidz 10281 addmodlteq 10393 frec2uzrand 10400 expcan 10689 nn0opthd 10695 fz1eqb 10763 cj11 10907 sqrt0 11006 recan 11111 0dvds 11811 dvds1 11851 alzdvds 11852 nn0enne 11899 nn0oddm1d2 11906 nnoddm1d2 11907 divalgmod 11924 gcdeq0 11970 algcvgblem 12041 prmexpb 12143 ennnfonelemim 12417 grprcan 12842 grplcan 12864 grpinv11 12871 tgdom 13443 en1top 13448 hmeocnvb 13689 metrest 13877 lgsne0 14310 bj-nnbist 14356 bj-nnbidc 14369 bj-peano4 14567 bj-nn0sucALT 14590 |
Copyright terms: Public domain | W3C validator |