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  596  notbi  666  pm5.21  695  nbn2  697  2falsed  702  pm5.21ndd  705  oibabs  714  orbi2d  790  con4biddc  857  con1bidc  874  con1bdc  878  dedlema  969  dedlemb  970  xorbin  1384  albi  1468  19.21ht  1581  exbi  1604  19.23t  1677  equequ1  1712  equequ2  1713  equsexd  1729  dral1  1730  cbv2h  1748  cbv2w  1750  sbequ12  1771  sbiedh  1787  drex1  1798  ax11b  1826  sbequ  1840  sbft  1848  sb56  1885  cbvexdh  1926  eupickb  2107  eupickbi  2108  elequ1  2152  elequ2  2153  ceqsalt  2763  ceqex  2864  mob2  2917  euxfr2dc  2922  reu6  2926  sbciegft  2993  csbiebt  3096  sseq1  3178  reupick  3419  reupick2  3421  disjeq2  3984  disjeq1  3987  exmidsssnc  4203  copsexg  4244  euotd  4254  poeq2  4300  sotritric  4324  sotritrieq  4325  seeq1  4339  seeq2  4340  alxfr  4461  ralxfrd  4462  rexxfrd  4463  ordelsuc  4504  sosng  4699  iss  4953  iotaval  5189  funeq  5236  funssres  5258  f0dom0  5409  tz6.12c  5545  fnbrfvb  5556  ssimaex  5577  fvimacnv  5631  elpreima  5635  fsn  5688  fconst2g  5731  elunirn  5766  f1ocnvfvb  5780  foeqcnvco  5790  f1eqcocnv  5791  fliftfun  5796  isose  5821  isopo  5823  isoso  5825  f1oiso2  5827  eusvobj2  5860  oprabid  5906  f1opw2  6076  op1steq  6179  rntpos  6257  frecabcl  6399  nnsucelsuc  6491  nnsucsssuc  6492  nnsseleq  6501  nnaord  6509  nnmord  6517  nnaordex  6528  nnawordex  6529  nnm00  6530  erexb  6559  swoord1  6563  swoord2  6564  iinerm  6606  fundmen  6805  mapxpen  6847  ssenen  6850  nneneq  6856  nndomo  6863  fidifsnen  6869  en1eqsnbi  6947  suplub2ti  6999  isoti  7005  ordiso2  7033  ordiso  7034  ctm  7107  ctssdc  7111  enomni  7136  enmkv  7159  enwomni  7167  pm54.43  7188  pr2ne  7190  ltexnqq  7406  genprndl  7519  genprndu  7520  nqprl  7549  nqpru  7550  1idprl  7588  1idpru  7589  ltexprlemrnd  7603  ltaprg  7617  recexprlemrnd  7627  cauappcvgprlemrnd  7648  caucvgprlemrnd  7671  caucvgprprlemrnd  7699  suplocexprlemrl  7715  suplocexprlemru  7717  map2psrprg  7803  ltxrlt  8022  lttri3  8036  addlsub  8326  addid0  8329  ltadd2  8375  eqord1  8439  reapti  8535  apreap  8543  ltmul1  8548  apreim  8559  ltleap  8588  mulap0b  8611  recapb  8627  apmul1  8744  rerecapb  8799  lt2msq  8842  nnsub  8957  zltnle  9298  zleloe  9299  zrevaddcl  9302  zltp1le  9306  zapne  9326  nn0n0n1ge2b  9331  zdiv  9340  nneo  9355  zeo2  9358  qrevaddcl  9643  npnflt  9814  nmnfgt  9817  xltneg  9835  xleadd1  9874  iccid  9924  zltaddlt1le  10006  fzn  10041  0fz1  10044  uzsplit  10091  fzm1  10099  fzrevral  10104  ssfzo12bi  10224  qltnle  10245  ioo0  10259  ioom  10260  ico0  10261  ioc0  10262  flqge  10281  modqid2  10350  modqmuladd  10365  frec2uzlt2d  10403  qsqeqor  10630  nn0ltexp2  10688  shftlem  10824  shftuz  10825  caucvgrelemcau  10988  sqrtsq  11052  abs00ap  11070  cau3lem  11122  maxleb  11224  rexico  11229  negfi  11235  climshft  11311  zsumdc  11391  fsum3  11394  fsum00  11469  zproddc  11586  fprodseq  11590  dvdsval2  11796  moddvds  11805  negdvdsb  11813  dvdsnegb  11814  dvdscmulr  11826  dvdsmulcr  11827  dvdssub2  11841  fzo0dvdseq  11862  ltoddhalfle  11897  dvdsgcdb  12013  gcdzeq  12022  dvdssqlem  12030  lcmeq0  12070  lcmdvdsb  12083  coprmgcdb  12087  ncoprmgcdne1b  12088  cncongr  12104  isprm2lem  12115  dvdsprime  12121  dvdsprm  12136  coprm  12143  euclemma  12145  rpexp  12152  prmdiveq  12235  hashgcdlem  12237  odzdvds  12244  pythagtrip  12282  pcdvdsb  12318  pc2dvds  12328  pcprmpw2  12331  pcprmpw  12332  enct  12433  intopsn  12785  isgrpid2  12912  isgrpinv  12925  ringinvnz1ne0  13224  ringinvnzdiv  13225  unitmulclb  13281  dvreq1  13309  toponcomb  13498  tgss3  13548  isopn3  13595  neiint  13615  neipsm  13624  opnneissb  13625  opnssneib  13626  tpnei  13630  opnneiid  13634  restopnb  13651  tgcn  13678  tgcnp  13679  iscnp4  13688  cnpnei  13689  cnntr  13695  lmss  13716  upxp  13742  txcn  13745  txlm  13749  hmeoopn  13781  hmeocld  13782  xblm  13887  blssexps  13899  blssex  13900  isxms2  13922  neibl  13961  metss  13964  metrest  13976  metcnp3  13981  ivthinclemlr  14085  ivthinclemur  14087  cnplimccntop  14109  eflt  14166  lgsdir2lem4  14402  lgsne0  14409  m1lgs  14422  bj-charfunbi  14533  subctctexmid  14720  triap  14747  iswomni0  14769