Theorem impbii 126

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
impbii.1	⊢ (𝜑 → 𝜓)
impbii.2	⊢ (𝜓 → 𝜑)

Assertion

Ref	Expression
impbii	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2 ⊢ (𝜑 → 𝜓)
2		impbii.2	. 2 ⊢ (𝜓 → 𝜑)
3		bi3 119	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  392  anass  405  pm5.32  457  jcab  611  notnotnot  643  con2b  679  imnan  701  2false  713  pm5.21nii  716  pm4.8  719  oibabs  726  orcom  740  ioran  764  oridm  769  orbi2i  774  or12  778  pm4.44  791  ordi  828  andi  830  pm4.72  839  stdcndc  857  stdcndcOLD  858  stdcn  859  dcnn  860  pm4.82  963  rnlem  989  3jaob  1343  xoranor  1426  falantru  1452  3impexp  1487  3impexpbicom  1488  alcom  1531  19.26  1534  19.3h  1606  19.3  1607  19.21h  1610  19.43  1681  19.9h  1696  excom  1716  19.41h  1737  19.41  1738  equcom  1758  equsalh  1778  equsex  1780  cbvalv1  1804  cbvexv1  1805  cbvalh  1806  cbvexh  1808  sbbii  1818  sbh  1829  equs45f  1855  sb6f  1856  sbcof2  1863  sbequ8  1900  sbidm  1904  sb5rf  1905  sb6rf  1906  equvin  1916  sbimv  1948  cbvalvw  1975  cbvexvw  1976  sbalyz  2059  eu2  2131  eu3h  2132  eu5  2134  mo3h  2140  euan  2143  axext4  2222  cleqh  2338  r19.26  2677  ralcom3  2719  ceqsex  2860  gencbvex  2869  gencbvex2  2870  gencbval  2871  eqvinc  2949  pm13.183  2964  rr19.3v  2965  rr19.28v  2966  reu6  3015  reu3  3016  sbnfc2  3208  difdif  3354  ddifnel  3360  ddifstab  3361  ssddif  3465  difin  3468  uneqin  3482  indifdir  3487  undif3ss  3492  difrab  3507  un00  3567  vvin  3569  undifss  3608  ssdifeq0  3610  ralidm  3628  ralf0  3630  ralm  3631  elpr2  3731  snidb  3739  rabsnifsb  3777  difsnb  3858  preq12b  3895  preqsn  3900  axpweq  4310  exmidn0m  4340  exmidsssn  4341  exmid0el  4343  exmidel  4344  exmidundif  4345  exmidundifim  4346  sspwb  4358  unipw  4359  opm  4376  opth  4379  ssopab2b  4421  elon2  4523  unexb  4590  eusvnfb  4602  eusv2nf  4604  ralxfrALT  4615  uniexb  4621  iunpw  4628  onsucb  4652  unon  4660  sucprcreg  4698  opthreg  4705  ordsuc  4712  dcextest  4730  peano2b  4764  opelxp  4806  opthprc  4828  relop  4932  issetid  4936  xpid11  5007  elres  5101  iss  5112  issref  5173  xpmlem  5211  sqxpeq0  5214  ssrnres  5233  dfrel2  5241  relrelss  5317  fn0  5506  funssxp  5560  f00  5587  f0bi  5588  dffo2  5622  ffoss  5675  f1o00  5679  fo00  5680  fv3  5721  dff2  5855  dffo4  5859  dffo5  5860  fmpt  5861  ffnfv  5869  fsn  5883  fsn2  5885  funop  5895  isores1  6023  ssoprab2b  6148  eqfnov2  6199  cnvoprab  6474  reldmtpos  6529  mapsn  6978  mapsncnv  6983  mptelixpg  7022  elixpsn  7023  ixpsnf1o  7024  en0  7088  en1  7092  modom  7114  dom0  7144  exmidpw  7221  exmidpweq  7222  pw1fin  7223  exmidpw2en  7225  undifdcss  7236  exmidssfi  7252  residfi  7260  fidcenum  7280  djuexb  7390  ctssdc  7459  exmidomni  7488  nninfinfwlpo  7526  nninfwlpo  7527  exmidfodomr  7562  iftrueb01  7588  exmidontri  7604  exmidontri2or  7608  onntri3or  7610  onntri2or  7611  dftap2  7623  exmidmotap  7633  elni2  7687  ltbtwnnqq  7788  enq0ref  7806  elnp1st2nd  7849  elrealeu  8202  elreal2  8203  le2tri3i  8441  elnn0nn  9616  elnnnn0b  9618  elnnnn0c  9619  elnnz  9663  elnn0z  9666  elnnz1  9676  elz2  9725  eluz2b2  10018  elnn1uz2  10022  elpqb  10066  elioo4g  10352  eluzfz2b  10453  fzm  10458  elfz1end  10477  fzass4  10484  elfz1b  10513  fz01or  10534  nn0fz0  10542  fzolb  10577  fzom  10588  elfzo0  10609  fzo1fzo0n0  10611  elfzo0z  10612  elfzo1  10619  infssuzex  10682  hashf1  11308  hash2en  11316  wrdexb  11337  0wrd0  11351  rexanuz  11775  rexuz3  11777  sqrt0rlem  11790  fisum0diag  12232  fprod0diagfz  12419  isprm6  12950  nnoddn2prmb  13069  4sqlem4  13199  4sqexercise1  13205  ballotfilem2  13285  ballotfilemrinv  13334  ballotfilemth  13338  ennnfone  13373  ctinfom  13376  ctinf  13378  fnpr2ob  13719  dfgrp2  13890  dfgrp3m  13962  dfgrp3me  13963  isnsg3  14068  invghm  14222  dvdsrzring  15046  zrhval  15060  tgclb  15308  xmetunirn  15601  dich0  15895  elply2  15978  2sqlem2  16456  umgrislfupgrenlem  16593  umgrislfupgrdom  16594  uspgrupgrushgr  16645  usgrumgruspgr  16648  usgruspgrben  16649  usgrislfuspgrdom  16653  clwwlkn1loopb  16883  dichmul0or  16982  bj-nnsn  16983  bdeq  17071  bdop  17123  bdunexb  17168  bj-2inf  17186  bj-nn0suc  17212  pw1dceq  17257  exmidnotnotr  17258  exmidcon  17259  exmidpeirce  17260  wexmiddiffi  17266  wexmiddifxy  17268  idjudju  17269  nnnninfen  17287  exmidsbth  17292  trirec0  17317  redc0  17331  reap0  17332  cndcap  17333  neap0mkv  17343