Theorem impbid 129

Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	1, 2	impbid21d 128	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 49	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:  bicom1  131  impbid1  142  pm5.74  179  imbi1d  231  pm5.501  244  pm5.32d  450  impbida  598  notbi  670  pm5.21  700  nbn2  702  2falsed  707  pm5.21ndd  710  oibabs  719  orbi2d  795  con4biddc  862  con1bidc  879  con1bdc  883  dedlema  975  dedlemb  976  xorbin  1426  albi  1514  19.21ht  1627  exbi  1650  19.23t  1723  equequ1  1758  equequ2  1759  equsexd  1775  dral1  1776  cbv2h  1794  cbv2w  1796  sbequ12  1817  sbiedh  1833  drex1  1844  ax11b  1872  sbequ  1886  sbft  1894  sb56  1932  cbvexdh  1973  eupickb  2159  eupickbi  2160  elequ1  2204  elequ2  2205  ceqsalt  2826  ceqex  2930  mob2  2983  euxfr2dc  2988  reu6  2992  sbciegft  3059  csbiebt  3164  sseq1  3247  reupick  3488  reupick2  3490  disjeq2  4063  disjeq1  4066  exmidsssnc  4287  copsexg  4330  euotd  4341  poeq2  4391  sotritric  4415  sotritrieq  4416  seeq1  4430  seeq2  4431  alxfr  4552  ralxfrd  4553  rexxfrd  4554  ordelsuc  4597  sosng  4792  iss  5051  iotaval  5290  funeq  5338  funssres  5360  f0dom0  5521  tz6.12c  5659  fnbrfvb  5674  ssimaex  5697  fvimacnv  5752  elpreima  5756  fsn  5809  fconst2g  5858  elunirn  5896  f1ocnvfvb  5910  foeqcnvco  5920  f1eqcocnv  5921  fliftfun  5926  isose  5951  isopo  5953  isoso  5955  f1oiso2  5957  eusvobj2  5993  oprabid  6039  f1opw2  6218  op1steq  6331  rntpos  6409  frecabcl  6551  nnsucelsuc  6645  nnsucsssuc  6646  nnsseleq  6655  nnaord  6663  nnmord  6671  nnaordex  6682  nnawordex  6683  nnm00  6684  erexb  6713  swoord1  6717  swoord2  6718  iinerm  6762  fundmen  6967  dom1o  6985  mapxpen  7017  ssenen  7020  nneneq  7026  nndomo  7033  fidifsnen  7040  en1eqsnbi  7127  suplub2ti  7179  isoti  7185  ordiso2  7213  ordiso  7214  ctm  7287  ctssdc  7291  enomni  7317  enmkv  7340  enwomni  7348  pm54.43  7374  pr2ne  7376  ltexnqq  7606  genprndl  7719  genprndu  7720  nqprl  7749  nqpru  7750  1idprl  7788  1idpru  7789  ltexprlemrnd  7803  ltaprg  7817  recexprlemrnd  7827  cauappcvgprlemrnd  7848  caucvgprlemrnd  7871  caucvgprprlemrnd  7899  suplocexprlemrl  7915  suplocexprlemru  7917  map2psrprg  8003  ltxrlt  8223  lttri3  8237  addlsub  8527  addid0  8530  ltadd2  8577  eqord1  8641  reapti  8737  apreap  8745  ltmul1  8750  apreim  8761  ltleap  8790  mulap0b  8813  recapb  8829  apmul1  8946  rerecapb  9001  lt2msq  9044  nnsub  9160  zltnle  9503  zleloe  9504  zrevaddcl  9508  zltp1le  9512  zapne  9532  nn0n0n1ge2b  9537  zdiv  9546  nneo  9561  zeo2  9564  qrevaddcl  9851  npnflt  10023  nmnfgt  10026  xltneg  10044  xleadd1  10083  iccid  10133  zltaddlt1le  10215  fzn  10250  0fz1  10253  uzsplit  10300  fzm1  10308  fzrevral  10313  ssfzo12bi  10443  qltnle  10475  ioo0  10491  ioom  10492  ico0  10493  ioc0  10494  flqge  10514  modqid2  10585  modqmuladd  10600  frec2uzlt2d  10638  seqf1oglem1  10753  qsqeqor  10884  nn0ltexp2  10943  len0nnbi  11119  ccats1pfxeqbi  11290  reuccatpfxs1  11295  shftlem  11343  shftuz  11344  caucvgrelemcau  11507  sqrtsq  11571  abs00ap  11589  cau3lem  11641  maxleb  11743  rexico  11748  negfi  11755  climshft  11831  zsumdc  11911  fsum3  11914  fsum00  11989  zproddc  12106  fprodseq  12110  dvdsval2  12317  moddvds  12326  negdvdsb  12334  dvdsnegb  12335  dvdscmulr  12347  dvdsmulcr  12348  dvdssub2  12362  fzo0dvdseq  12384  ltoddhalfle  12420  dvdsgcdb  12550  gcdzeq  12559  dvdssqlem  12567  lcmeq0  12609  lcmdvdsb  12622  coprmgcdb  12626  ncoprmgcdne1b  12627  cncongr  12643  isprm2lem  12654  dvdsprime  12660  dvdsprm  12675  coprm  12682  euclemma  12684  rpexp  12691  prmdiveq  12774  hashgcdlem  12776  odzdvds  12784  pythagtrip  12822  pcdvdsb  12859  pc2dvds  12869  pcprmpw2  12872  pcprmpw  12873  enct  13020  intopsn  13416  gsumfzval  13440  isgrpid2  13589  isgrpinv  13603  f1ghm0to0  13825  ringinvnz1ne0  14028  ringinvnzdiv  14029  unitmulclb  14094  dvreq1  14122  isnzr2  14164  rrgeq0  14245  domneq0  14252  lssats2  14394  lspsneq0  14406  znunit  14639  toponcomb  14718  tgss3  14768  isopn3  14815  neiint  14835  neipsm  14844  opnneissb  14845  opnssneib  14846  tpnei  14850  opnneiid  14854  restopnb  14871  tgcn  14898  tgcnp  14899  iscnp4  14908  cnpnei  14909  cnntr  14915  lmss  14936  upxp  14962  txcn  14965  txlm  14969  hmeoopn  15001  hmeocld  15002  xblm  15107  blssexps  15119  blssex  15120  isxms2  15142  neibl  15181  metss  15184  metrest  15196  metcnp3  15201  ivthinclemlr  15327  ivthinclemur  15329  cnplimccntop  15360  eflt  15465  dvdsppwf1o  15679  lgsdir2lem4  15726  lgsne0  15733  gausslemma2dlem1a  15753  lgsquadlem1  15772  m1lgs  15780  uhgr0vb  15900  ausgrusgrben  15982  ushgredgedg  16040  ushgredgedgloop  16042  loopclwwlkn1b  16161  bj-charfunbi  16257  subctctexmid  16453  triap  16485  iswomni0  16507