Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impbii | GIF version |
Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
impbii.1 | ⊢ (𝜑 → 𝜓) |
impbii.2 | ⊢ (𝜓 → 𝜑) |
Ref | Expression |
---|---|
impbii | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbii.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | impbii.2 | . 2 ⊢ (𝜓 → 𝜑) | |
3 | bi3 118 | . 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓))) | |
4 | 1, 2, 3 | mp2 16 | 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: bicom 139 biid 170 2th 173 pm5.74 178 bitri 183 bibi2i 226 bi2.04 247 pm5.4 248 imdi 249 impexp 261 ancom 264 pm4.45im 332 dfbi2 386 anass 399 pm5.32 449 jcab 593 notnotnot 624 con2b 659 imnan 680 2false 691 pm5.21nii 694 pm4.8 697 oibabs 704 orcom 718 ioran 742 oridm 747 orbi2i 752 or12 756 pm4.44 769 ordi 806 andi 808 pm4.72 817 stdcndc 835 stdcndcOLD 836 stdcn 837 dcnn 838 pm4.82 939 rnlem 965 3jaob 1291 xoranor 1366 falantru 1392 3impexp 1424 3impexpbicom 1425 alcom 1465 19.26 1468 19.3h 1540 19.3 1541 19.21h 1544 19.43 1615 19.9h 1630 excom 1651 19.41h 1672 19.41 1673 equcom 1693 equsalh 1713 equsex 1715 cbvalv1 1738 cbvexv1 1739 cbvalh 1740 cbvexh 1742 sbbii 1752 sbh 1763 equs45f 1789 sb6f 1790 sbcof2 1797 sbequ8 1834 sbidm 1838 sb5rf 1839 sb6rf 1840 equvin 1850 sbimv 1880 cbvalvw 1906 cbvexvw 1907 sbalyz 1986 eu2 2057 eu3h 2058 eu5 2060 mo3h 2066 euan 2069 axext4 2148 cleqh 2264 r19.26 2590 ralcom3 2631 ceqsex 2759 gencbvex 2767 gencbvex2 2768 gencbval 2769 eqvinc 2844 pm13.183 2859 rr19.3v 2860 rr19.28v 2861 reu6 2910 reu3 2911 sbnfc2 3100 difdif 3242 ddifnel 3248 ddifstab 3249 ssddif 3351 difin 3354 uneqin 3368 indifdir 3373 undif3ss 3378 difrab 3391 un00 3450 undifss 3484 ssdifeq0 3486 ralidm 3504 ralf0 3507 ralm 3508 elpr2 3592 snidb 3600 difsnb 3710 preq12b 3744 preqsn 3749 axpweq 4144 exmidn0m 4174 exmidsssn 4175 exmid0el 4177 exmidel 4178 exmidundif 4179 exmidundifim 4180 sspwb 4188 unipw 4189 opm 4206 opth 4209 ssopab2b 4248 elon2 4348 unexb 4414 eusvnfb 4426 eusv2nf 4428 ralxfrALT 4439 uniexb 4445 iunpw 4452 sucelon 4474 unon 4482 sucprcreg 4520 opthreg 4527 ordsuc 4534 dcextest 4552 peano2b 4586 opelxp 4628 opthprc 4649 relop 4748 issetid 4752 xpid11 4821 elres 4914 iss 4924 issref 4980 xpmlem 5018 sqxpeq0 5021 ssrnres 5040 dfrel2 5048 relrelss 5124 fn0 5301 funssxp 5351 f00 5373 f0bi 5374 dffo2 5408 ffoss 5458 f1o00 5461 fo00 5462 fv3 5503 dff2 5623 dffo4 5627 dffo5 5628 fmpt 5629 ffnfv 5637 fsn 5651 fsn2 5653 isores1 5776 ssoprab2b 5890 eqfnov2 5940 cnvoprab 6193 reldmtpos 6212 mapsn 6647 mapsncnv 6652 mptelixpg 6691 elixpsn 6692 ixpsnf1o 6693 en0 6752 en1 6756 dom0 6795 exmidpw 6865 exmidpweq 6866 pw1fin 6867 undifdcss 6879 fidcenum 6912 djuexb 7000 ctssdc 7069 exmidomni 7097 exmidfodomr 7151 exmidontri 7186 exmidontri2or 7190 onntri3or 7192 onntri2or 7193 elni2 7246 ltbtwnnqq 7347 enq0ref 7365 elnp1st2nd 7408 elrealeu 7761 elreal2 7762 le2tri3i 7998 elnn0nn 9147 elnnnn0b 9149 elnnnn0c 9150 elnnz 9192 elnn0z 9195 elnnz1 9205 elz2 9253 eluz2b2 9532 elnn1uz2 9536 elpqb 9578 elioo4g 9861 eluzfz2b 9958 fzm 9963 elfz1end 9980 fzass4 9987 elfz1b 10015 fz01or 10036 nn0fz0 10044 fzolb 10078 fzom 10089 elfzo0 10107 fzo1fzo0n0 10108 elfzo0z 10109 elfzo1 10115 rexanuz 10916 rexuz3 10918 sqrt0rlem 10931 fisum0diag 11368 fprod0diagfz 11555 infssuzex 11867 isprm6 12058 oddpwdclemdc 12084 nnoddn2prmb 12173 ennnfone 12301 ctinfom 12304 ctinf 12306 tgclb 12612 xmetunirn 12905 bj-nnsn 13457 bdeq 13546 bdop 13598 bdunexb 13643 bj-2inf 13661 bj-nn0suc 13687 exmidsbth 13744 trirec0 13764 redc0 13777 reap0 13778 |
Copyright terms: Public domain | W3C validator |