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 ⊢ (𝜑 ↔ 𝜓)

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  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  3566  vvin  3568  undifss  3605  ssdifeq0  3607  ralidm  3625  ralf0  3627  ralm  3628  elpr2  3727  snidb  3735  rabsnifsb  3773  difsnb  3853  preq12b  3890  preqsn  3895  axpweq  4303  exmidn0m  4333  exmidsssn  4334  exmid0el  4336  exmidel  4337  exmidundif  4338  exmidundifim  4339  sspwb  4351  unipw  4352  opm  4369  opth  4372  ssopab2b  4414  elon2  4516  unexb  4583  eusvnfb  4595  eusv2nf  4597  ralxfrALT  4608  uniexb  4614  iunpw  4621  onsucb  4645  unon  4653  sucprcreg  4691  opthreg  4698  ordsuc  4705  dcextest  4723  peano2b  4757  opelxp  4799  opthprc  4821  relop  4925  issetid  4929  xpid11  5000  elres  5094  iss  5104  issref  5165  xpmlem  5203  sqxpeq0  5206  ssrnres  5225  dfrel2  5233  relrelss  5309  fn0  5498  funssxp  5552  f00  5579  f0bi  5580  dffo2  5614  ffoss  5667  f1o00  5671  fo00  5672  fv3  5713  dff2  5843  dffo4  5847  dffo5  5848  fmpt  5849  ffnfv  5857  fsn  5871  fsn2  5873  funop  5883  isores1  6010  ssoprab2b  6135  eqfnov2  6186  cnvoprab  6460  reldmtpos  6514  mapsn  6962  mapsncnv  6967  mptelixpg  7006  elixpsn  7007  ixpsnf1o  7008  en0  7072  en1  7076  modom  7098  dom0  7128  exmidpw  7205  exmidpweq  7206  pw1fin  7207  exmidpw2en  7209  undifdcss  7220  exmidssfi  7236  residfi  7244  fidcenum  7263  djuexb  7374  ctssdc  7443  exmidomni  7472  nninfinfwlpo  7510  nninfwlpo  7511  exmidfodomr  7546  iftrueb01  7572  exmidontri  7588  exmidontri2or  7592  onntri3or  7594  onntri2or  7595  dftap2  7607  exmidmotap  7617  elni2  7671  ltbtwnnqq  7772  enq0ref  7790  elnp1st2nd  7833  elrealeu  8186  elreal2  8187  le2tri3i  8424  elnn0nn  9584  elnnnn0b  9586  elnnnn0c  9587  elnnz  9633  elnn0z  9636  elnnz1  9646  elz2  9695  eluz2b2  9982  elnn1uz2  9986  elpqb  10029  elioo4g  10315  eluzfz2b  10416  fzm  10421  elfz1end  10439  fzass4  10446  elfz1b  10475  fz01or  10496  nn0fz0  10504  fzolb  10539  fzom  10550  elfzo0  10571  fzo1fzo0n0  10573  elfzo0z  10574  elfzo1  10581  infssuzex  10644  hashf1  11265  hash2en  11273  wrdexb  11294  0wrd0  11308  rexanuz  11732  rexuz3  11734  sqrt0rlem  11747  fisum0diag  12186  fprod0diagfz  12373  isprm6  12903  oddpwdclemdc  12929  nnoddn2prmb  13019  4sqlem4  13149  4sqexercise1  13155  ballotfilem2  13206  ballotfilemrinv  13255  ballotfilemth  13259  ennnfone  13294  ctinfom  13297  ctinf  13299  fnpr2ob  13638  dfgrp2  13809  dfgrp3m  13881  dfgrp3me  13882  isnsg3  13987  invghm  14110  dvdsrzring  14910  zrhval  14924  tgclb  15089  xmetunirn  15382  dich0  15676  elply2  15759  2sqlem2  16148  umgrislfupgrenlem  16285  umgrislfupgrdom  16286  uspgrupgrushgr  16337  usgrumgruspgr  16340  usgruspgrben  16341  usgrislfuspgrdom  16345  clwwlkn1loopb  16575  dichmul0or  16674  bj-nnsn  16675  bdeq  16763  bdop  16815  bdunexb  16860  bj-2inf  16878  bj-nn0suc  16904  pw1dceq  16948  exmidnotnotr  16949  exmidcon  16950  exmidpeirce  16951  nnnninfen  16969  exmidsbth  16974  trirec0  16998  redc0  17012  reap0  17013  cndcap  17014  neap0mkv  17024