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 385 anass 398 pm5.32 448 jcab 577 notnotnot 608 con2b 643 imnan 664 2false 675 pm5.21nii 678 pm4.8 681 oibabs 688 orcom 702 ioran 726 oridm 731 orbi2i 736 or12 740 pm4.44 753 ordi 790 andi 792 pm4.72 797 stdcndc 815 stdcndcOLD 816 stdcn 817 dcnn 818 pm4.82 919 rnlem 945 3jaob 1265 xoranor 1340 falantru 1366 3impexp 1398 3impexpbicom 1399 alcom 1439 19.26 1442 19.3h 1517 19.3 1518 19.21h 1521 19.43 1592 19.9h 1607 excom 1627 19.41h 1648 19.41 1649 equcom 1667 equsalh 1689 equsex 1691 cbvalh 1711 cbvexh 1713 sbbii 1723 sbh 1734 equs45f 1758 sb6f 1759 sbcof2 1766 sbequ8 1803 sbidm 1807 sb5rf 1808 sb6rf 1809 equvin 1819 sbimv 1849 sbalyz 1952 eu2 2021 eu3h 2022 eu5 2024 mo3h 2030 euan 2033 axext4 2101 cleqh 2217 r19.26 2535 ralcom3 2575 ceqsex 2698 gencbvex 2706 gencbvex2 2707 gencbval 2708 eqvinc 2782 pm13.183 2796 rr19.3v 2797 rr19.28v 2798 reu6 2846 reu3 2847 sbnfc2 3030 difdif 3171 ddifnel 3177 ddifstab 3178 ssddif 3280 difin 3283 uneqin 3297 indifdir 3302 undif3ss 3307 difrab 3320 un00 3379 undifss 3413 ssdifeq0 3415 ralidm 3433 ralf0 3436 ralm 3437 elpr2 3519 snidb 3525 difsnb 3633 preq12b 3667 preqsn 3672 axpweq 4065 exmidn0m 4094 exmidsssn 4095 exmid0el 4097 exmidel 4098 exmidundif 4099 exmidundifim 4100 sspwb 4108 unipw 4109 opm 4126 opth 4129 ssopab2b 4168 elon2 4268 unexb 4333 eusvnfb 4345 eusv2nf 4347 ralxfrALT 4358 uniexb 4364 iunpw 4371 sucelon 4389 unon 4397 sucprcreg 4434 opthreg 4441 ordsuc 4448 dcextest 4465 peano2b 4498 opelxp 4539 opthprc 4560 relop 4659 issetid 4663 xpid11 4732 elres 4825 iss 4835 issref 4891 xpmlem 4929 sqxpeq0 4932 ssrnres 4951 dfrel2 4959 relrelss 5035 fn0 5212 funssxp 5262 f00 5284 f0bi 5285 dffo2 5319 ffoss 5367 f1o00 5370 fo00 5371 fv3 5412 dff2 5532 dffo4 5536 dffo5 5537 fmpt 5538 ffnfv 5546 fsn 5560 fsn2 5562 isores1 5683 ssoprab2b 5796 eqfnov2 5846 cnvoprab 6099 reldmtpos 6118 mapsn 6552 mapsncnv 6557 mptelixpg 6596 elixpsn 6597 ixpsnf1o 6598 en0 6657 en1 6661 dom0 6700 exmidpw 6770 undifdcss 6779 fidcenum 6812 djuexb 6897 ctssdc 6966 exmidomni 6982 exmidfodomr 7028 elni2 7090 ltbtwnnqq 7191 enq0ref 7209 elnp1st2nd 7252 elrealeu 7605 elreal2 7606 le2tri3i 7840 elnn0nn 8987 elnnnn0b 8989 elnnnn0c 8990 elnnz 9032 elnn0z 9035 elnnz1 9045 elz2 9090 eluz2b2 9365 elnn1uz2 9369 elioo4g 9685 eluzfz2b 9781 fzm 9786 elfz1end 9803 fzass4 9810 elfz1b 9838 fz01or 9859 nn0fz0 9867 fzolb 9898 fzom 9909 elfzo0 9927 fzo1fzo0n0 9928 elfzo0z 9929 elfzo1 9935 rexanuz 10728 rexuz3 10730 sqrt0rlem 10743 fisum0diag 11178 infssuzex 11569 isprm6 11752 oddpwdclemdc 11778 ennnfone 11865 ctinfom 11868 ctinf 11870 tgclb 12161 xmetunirn 12454 bj-nnsn 12872 bdeq 12948 bdop 13000 bdunexb 13045 bj-2inf 13063 bj-nn0suc 13089 exmidsbth 13146 |
Copyright terms: Public domain | W3C validator |