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  5519  tz6.12c  5657  fnbrfvb  5672  ssimaex  5695  fvimacnv  5750  elpreima  5754  fsn  5807  fconst2g  5854  elunirn  5890  f1ocnvfvb  5904  foeqcnvco  5914  f1eqcocnv  5915  fliftfun  5920  isose  5945  isopo  5947  isoso  5949  f1oiso2  5951  eusvobj2  5987  oprabid  6033  f1opw2  6212  op1steq  6325  rntpos  6403  frecabcl  6545  nnsucelsuc  6637  nnsucsssuc  6638  nnsseleq  6647  nnaord  6655  nnmord  6663  nnaordex  6674  nnawordex  6675  nnm00  6676  erexb  6705  swoord1  6709  swoord2  6710  iinerm  6754  fundmen  6959  dom1o  6977  mapxpen  7009  ssenen  7012  nneneq  7018  nndomo  7025  fidifsnen  7032  en1eqsnbi  7116  suplub2ti  7168  isoti  7174  ordiso2  7202  ordiso  7203  ctm  7276  ctssdc  7280  enomni  7306  enmkv  7329  enwomni  7337  pm54.43  7363  pr2ne  7365  ltexnqq  7595  genprndl  7708  genprndu  7709  nqprl  7738  nqpru  7739  1idprl  7777  1idpru  7778  ltexprlemrnd  7792  ltaprg  7806  recexprlemrnd  7816  cauappcvgprlemrnd  7837  caucvgprlemrnd  7860  caucvgprprlemrnd  7888  suplocexprlemrl  7904  suplocexprlemru  7906  map2psrprg  7992  ltxrlt  8212  lttri3  8226  addlsub  8516  addid0  8519  ltadd2  8566  eqord1  8630  reapti  8726  apreap  8734  ltmul1  8739  apreim  8750  ltleap  8779  mulap0b  8802  recapb  8818  apmul1  8935  rerecapb  8990  lt2msq  9033  nnsub  9149  zltnle  9492  zleloe  9493  zrevaddcl  9497  zltp1le  9501  zapne  9521  nn0n0n1ge2b  9526  zdiv  9535  nneo  9550  zeo2  9553  qrevaddcl  9839  npnflt  10011  nmnfgt  10014  xltneg  10032  xleadd1  10071  iccid  10121  zltaddlt1le  10203  fzn  10238  0fz1  10241  uzsplit  10288  fzm1  10296  fzrevral  10301  ssfzo12bi  10431  qltnle  10463  ioo0  10479  ioom  10480  ico0  10481  ioc0  10482  flqge  10502  modqid2  10573  modqmuladd  10588  frec2uzlt2d  10626  seqf1oglem1  10741  qsqeqor  10872  nn0ltexp2  10931  len0nnbi  11106  ccats1pfxeqbi  11274  reuccatpfxs1  11279  shftlem  11327  shftuz  11328  caucvgrelemcau  11491  sqrtsq  11555  abs00ap  11573  cau3lem  11625  maxleb  11727  rexico  11732  negfi  11739  climshft  11815  zsumdc  11895  fsum3  11898  fsum00  11973  zproddc  12090  fprodseq  12094  dvdsval2  12301  moddvds  12310  negdvdsb  12318  dvdsnegb  12319  dvdscmulr  12331  dvdsmulcr  12332  dvdssub2  12346  fzo0dvdseq  12368  ltoddhalfle  12404  dvdsgcdb  12534  gcdzeq  12543  dvdssqlem  12551  lcmeq0  12593  lcmdvdsb  12606  coprmgcdb  12610  ncoprmgcdne1b  12611  cncongr  12627  isprm2lem  12638  dvdsprime  12644  dvdsprm  12659  coprm  12666  euclemma  12668  rpexp  12675  prmdiveq  12758  hashgcdlem  12760  odzdvds  12768  pythagtrip  12806  pcdvdsb  12843  pc2dvds  12853  pcprmpw2  12856  pcprmpw  12857  enct  13004  intopsn  13400  gsumfzval  13424  isgrpid2  13573  isgrpinv  13587  f1ghm0to0  13809  ringinvnz1ne0  14012  ringinvnzdiv  14013  unitmulclb  14078  dvreq1  14106  isnzr2  14148  rrgeq0  14229  domneq0  14236  lssats2  14378  lspsneq0  14390  znunit  14623  toponcomb  14702  tgss3  14752  isopn3  14799  neiint  14819  neipsm  14828  opnneissb  14829  opnssneib  14830  tpnei  14834  opnneiid  14838  restopnb  14855  tgcn  14882  tgcnp  14883  iscnp4  14892  cnpnei  14893  cnntr  14899  lmss  14920  upxp  14946  txcn  14949  txlm  14953  hmeoopn  14985  hmeocld  14986  xblm  15091  blssexps  15103  blssex  15104  isxms2  15126  neibl  15165  metss  15168  metrest  15180  metcnp3  15185  ivthinclemlr  15311  ivthinclemur  15313  cnplimccntop  15344  eflt  15449  dvdsppwf1o  15663  lgsdir2lem4  15710  lgsne0  15717  gausslemma2dlem1a  15737  lgsquadlem1  15756  m1lgs  15764  uhgr0vb  15884  ausgrusgrben  15966  ushgredgedg  16024  ushgredgedgloop  16026  bj-charfunbi  16174  subctctexmid  16366  triap  16397  iswomni0  16419