![]() |
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-1 5 ax-2 6 ax-mp 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 330 dfbi2 383 anass 396 pm5.32 446 jcab 575 notnotnot 606 con2b 641 imnan 662 2false 673 pm5.21nii 676 pm4.8 679 oibabs 686 orcom 700 ioran 724 oridm 729 orbi2i 734 or12 738 pm4.44 751 ordi 788 andi 790 pm4.72 795 stdcndc 813 stdcndcOLD 814 stdcn 815 dcnn 816 pm4.82 917 rnlem 943 3jaob 1263 xoranor 1338 falantru 1364 3impexp 1396 3impexpbicom 1397 alcom 1437 19.26 1440 19.3h 1515 19.3 1516 19.21h 1519 19.43 1590 19.9h 1605 excom 1625 19.41h 1646 19.41 1647 equcom 1665 equsalh 1687 equsex 1689 cbvalh 1709 cbvexh 1711 sbbii 1721 sbh 1732 equs45f 1756 sb6f 1757 sbcof2 1764 sbequ8 1801 sbidm 1805 sb5rf 1806 sb6rf 1807 equvin 1817 sbimv 1847 sbalyz 1950 eu2 2019 eu3h 2020 eu5 2022 mo3h 2028 euan 2031 axext4 2099 cleqh 2214 r19.26 2532 ralcom3 2572 ceqsex 2695 gencbvex 2703 gencbvex2 2704 gencbval 2705 eqvinc 2778 pm13.183 2792 rr19.3v 2793 rr19.28v 2794 reu6 2842 reu3 2843 sbnfc2 3026 difdif 3167 ddifnel 3173 ddifstab 3174 ssddif 3276 difin 3279 uneqin 3293 indifdir 3298 undif3ss 3303 difrab 3316 un00 3375 undifss 3409 ssdifeq0 3411 ralidm 3429 ralf0 3432 ralm 3433 elpr2 3515 snidb 3521 difsnb 3629 preq12b 3663 preqsn 3668 axpweq 4055 exmidn0m 4084 exmidsssn 4085 exmid0el 4087 exmidel 4088 exmidundif 4089 exmidundifim 4090 sspwb 4098 unipw 4099 opm 4116 opth 4119 ssopab2b 4158 elon2 4258 unexb 4323 eusvnfb 4335 eusv2nf 4337 ralxfrALT 4348 uniexb 4354 iunpw 4361 sucelon 4379 unon 4387 sucprcreg 4424 opthreg 4431 ordsuc 4438 dcextest 4455 peano2b 4488 opelxp 4529 opthprc 4550 relop 4649 issetid 4653 xpid11 4722 elres 4813 iss 4823 issref 4879 xpmlem 4917 sqxpeq0 4920 ssrnres 4939 dfrel2 4947 relrelss 5023 fn0 5200 funssxp 5250 f00 5272 f0bi 5273 dffo2 5307 ffoss 5355 f1o00 5358 fo00 5359 fv3 5398 dff2 5518 dffo4 5522 dffo5 5523 fmpt 5524 ffnfv 5532 fsn 5546 fsn2 5548 isores1 5669 ssoprab2b 5782 eqfnov2 5832 cnvoprab 6085 reldmtpos 6104 mapsn 6538 mapsncnv 6543 mptelixpg 6582 elixpsn 6583 ixpsnf1o 6584 en0 6643 en1 6647 dom0 6685 exmidpw 6755 undifdcss 6764 fidcenum 6796 djuexb 6881 ctssdc 6950 exmidomni 6964 exmidfodomr 7008 elni2 7070 ltbtwnnqq 7171 enq0ref 7189 elnp1st2nd 7232 elrealeu 7564 elreal2 7565 le2tri3i 7795 elnn0nn 8923 elnnnn0b 8925 elnnnn0c 8926 elnnz 8968 elnn0z 8971 elnnz1 8981 elz2 9026 eluz2b2 9299 elnn1uz2 9303 elioo4g 9610 eluzfz2b 9706 fzm 9711 elfz1end 9728 fzass4 9735 elfz1b 9763 fz01or 9784 nn0fz0 9792 fzolb 9823 fzom 9834 elfzo0 9852 fzo1fzo0n0 9853 elfzo0z 9854 elfzo1 9860 rexanuz 10652 rexuz3 10654 sqrt0rlem 10667 fisum0diag 11102 infssuzex 11490 isprm6 11671 oddpwdclemdc 11696 ennnfone 11783 ctinfom 11786 ctinf 11788 tgclb 12077 xmetunirn 12347 bj-nnsn 12638 bdeq 12713 bdop 12765 bdunexb 12810 bj-2inf 12828 bj-nn0suc 12854 exmidsbth 12911 |
Copyright terms: Public domain | W3C validator |