| 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 910 pm5.63dc 949 pm4.83dc 954 pm5.71dc 964 19.33b2 1652 19.9t 1665 sb4b 1857 a16gb 1888 euor2 2112 eupickbi 2136 ceqsalg 2800 eqvincg 2897 ddifstab 3305 csbprc 3506 undif4 3523 eqifdc 3607 ifnebibdc 3615 sssnm 3795 sneqbg 3804 opthpr 3813 elpwuni 4017 ss1o0el1 4241 exmid01 4242 exmidundif 4250 eusv2i 4502 reusv3 4507 iunpw 4527 suc11g 4605 ssxpbm 5118 ssxp1 5119 ssxp2 5120 xp11m 5121 2elresin 5387 mpteqb 5670 f1fveq 5841 f1elima 5842 f1imass 5843 fliftf 5868 nnsucuniel 6581 iserd 6646 ecopovtrn 6719 ecopover 6720 ecopovtrng 6722 ecopoverg 6723 map0g 6775 fopwdom 6933 f1finf1o 7049 mkvprop 7260 addcanpig 7447 mulcanpig 7448 srpospr 7896 readdcan 8212 cnegexlem1 8247 addcan 8252 addcan2 8253 neg11 8323 negreb 8337 add20 8547 cru 8675 mulcanapd 8734 uz11 9671 eqreznegel 9735 lbzbi 9737 xneg11 9956 xnn0xadd0 9989 xsubge0 10003 elioc2 10058 elico2 10059 elicc2 10060 fzopth 10183 2ffzeq 10263 flqidz 10429 addmodlteq 10543 frec2uzrand 10550 nninfinf 10588 expcan 10861 nn0opthd 10867 fz1eqb 10935 wrdnval 11024 eqwrd 11034 wrdl1s1 11084 cj11 11216 sqrt0 11315 recan 11420 0dvds 12122 dvds1 12164 alzdvds 12165 nn0enne 12213 nn0oddm1d2 12220 nnoddm1d2 12221 divalgmod 12238 gcdeq0 12298 algcvgblem 12371 prmexpb 12473 4sqexercise2 12722 4sqlemsdc 12723 4sqlem11 12724 ennnfonelemim 12795 grprcan 13369 grplcan 13394 grpinv11 13401 isnzr2 13946 znidomb 14420 tgdom 14544 en1top 14549 hmeocnvb 14790 metrest 14978 perfect 15473 lgsne0 15515 2lgs 15581 2lgsoddprmlem3 15588 bj-nnbist 15680 bj-nnbidc 15693 bj-peano4 15891 bj-nn0sucALT 15914 |
| Copyright terms: Public domain | W3C validator |