![]() |
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 119 | . 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓))) | |
4 | 1, 2, 3 | mp2 16 | 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: bicom 140 biid 171 2th 174 pm5.74 179 bitri 184 bibi2i 227 bi2.04 248 pm5.4 249 imdi 250 impexp 263 ancom 266 pm4.45im 334 dfbi2 388 anass 401 pm5.32 453 jcab 603 notnotnot 635 con2b 670 imnan 691 2false 702 pm5.21nii 705 pm4.8 708 oibabs 715 orcom 729 ioran 753 oridm 758 orbi2i 763 or12 767 pm4.44 780 ordi 817 andi 819 pm4.72 828 stdcndc 846 stdcndcOLD 847 stdcn 848 dcnn 849 pm4.82 952 rnlem 978 3jaob 1313 xoranor 1388 falantru 1414 3impexp 1448 3impexpbicom 1449 alcom 1489 19.26 1492 19.3h 1564 19.3 1565 19.21h 1568 19.43 1639 19.9h 1654 excom 1675 19.41h 1696 19.41 1697 equcom 1717 equsalh 1737 equsex 1739 cbvalv1 1762 cbvexv1 1763 cbvalh 1764 cbvexh 1766 sbbii 1776 sbh 1787 equs45f 1813 sb6f 1814 sbcof2 1821 sbequ8 1858 sbidm 1862 sb5rf 1863 sb6rf 1864 equvin 1874 sbimv 1905 cbvalvw 1931 cbvexvw 1932 sbalyz 2011 eu2 2082 eu3h 2083 eu5 2085 mo3h 2091 euan 2094 axext4 2173 cleqh 2289 r19.26 2616 ralcom3 2658 ceqsex 2790 gencbvex 2798 gencbvex2 2799 gencbval 2800 eqvinc 2875 pm13.183 2890 rr19.3v 2891 rr19.28v 2892 reu6 2941 reu3 2942 sbnfc2 3132 difdif 3275 ddifnel 3281 ddifstab 3282 ssddif 3384 difin 3387 uneqin 3401 indifdir 3406 undif3ss 3411 difrab 3424 un00 3484 undifss 3518 ssdifeq0 3520 ralidm 3538 ralf0 3541 ralm 3542 elpr2 3629 snidb 3637 difsnb 3750 preq12b 3785 preqsn 3790 axpweq 4189 exmidn0m 4219 exmidsssn 4220 exmid0el 4222 exmidel 4223 exmidundif 4224 exmidundifim 4225 sspwb 4234 unipw 4235 opm 4252 opth 4255 ssopab2b 4294 elon2 4394 unexb 4460 eusvnfb 4472 eusv2nf 4474 ralxfrALT 4485 uniexb 4491 iunpw 4498 onsucb 4520 unon 4528 sucprcreg 4566 opthreg 4573 ordsuc 4580 dcextest 4598 peano2b 4632 opelxp 4674 opthprc 4695 relop 4795 issetid 4799 xpid11 4868 elres 4961 iss 4971 issref 5029 xpmlem 5067 sqxpeq0 5070 ssrnres 5089 dfrel2 5097 relrelss 5173 fn0 5354 funssxp 5404 f00 5426 f0bi 5427 dffo2 5461 ffoss 5512 f1o00 5515 fo00 5516 fv3 5557 dff2 5681 dffo4 5685 dffo5 5686 fmpt 5687 ffnfv 5695 fsn 5709 fsn2 5711 isores1 5836 ssoprab2b 5953 eqfnov2 6004 cnvoprab 6259 reldmtpos 6278 mapsn 6716 mapsncnv 6721 mptelixpg 6760 elixpsn 6761 ixpsnf1o 6762 en0 6821 en1 6825 dom0 6866 exmidpw 6936 exmidpweq 6937 pw1fin 6938 exmidpw2en 6940 undifdcss 6951 fidcenum 6985 djuexb 7073 ctssdc 7142 exmidomni 7170 nninfwlpo 7207 exmidfodomr 7233 exmidontri 7268 exmidontri2or 7272 onntri3or 7274 onntri2or 7275 dftap2 7280 exmidmotap 7290 elni2 7343 ltbtwnnqq 7444 enq0ref 7462 elnp1st2nd 7505 elrealeu 7858 elreal2 7859 le2tri3i 8096 elnn0nn 9248 elnnnn0b 9250 elnnnn0c 9251 elnnz 9293 elnn0z 9296 elnnz1 9306 elz2 9354 eluz2b2 9633 elnn1uz2 9637 elpqb 9679 elioo4g 9964 eluzfz2b 10063 fzm 10068 elfz1end 10085 fzass4 10092 elfz1b 10120 fz01or 10141 nn0fz0 10149 fzolb 10183 fzom 10194 elfzo0 10212 fzo1fzo0n0 10213 elfzo0z 10214 elfzo1 10220 rexanuz 11029 rexuz3 11031 sqrt0rlem 11044 fisum0diag 11481 fprod0diagfz 11668 infssuzex 11982 isprm6 12179 oddpwdclemdc 12205 nnoddn2prmb 12294 4sqlem4 12424 4sqexercise1 12430 ennnfone 12476 ctinfom 12479 ctinf 12481 fnpr2ob 12816 dfgrp2 12971 dfgrp3m 13043 dfgrp3me 13044 isnsg3 13146 dvdsrzring 13902 tgclb 14022 xmetunirn 14315 2sqlem2 14920 bj-nnsn 14943 bdeq 15033 bdop 15085 bdunexb 15130 bj-2inf 15148 bj-nn0suc 15174 exmidsbth 15231 trirec0 15251 redc0 15264 reap0 15265 cndcap 15266 neap0mkv 15276 |
Copyright terms: Public domain | W3C validator |