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  600  notbi  672  pm5.21  703  nbn2  705  2falsed  710  pm5.21ndd  713  oibabs  722  orbi2d  798  con4biddc  865  con1bidc  882  con1bdc  886  dedlema  978  dedlemb  979  xorbin  1429  albi  1517  19.21ht  1630  exbi  1653  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1777  dral1  1778  cbv2h  1796  cbv2w  1798  sbequ12  1819  sbiedh  1835  drex1  1846  ax11b  1874  sbequ  1888  sbft  1896  sb56  1934  cbvexdh  1975  eupickb  2161  eupickbi  2162  elequ1  2206  elequ2  2207  ceqsalt  2830  ceqex  2934  mob2  2987  euxfr2dc  2992  reu6  2996  sbciegft  3063  csbiebt  3168  sseq1  3251  reupick  3493  reupick2  3495  disjeq2  4073  disjeq1  4076  exmidsssnc  4299  copsexg  4342  euotd  4353  poeq2  4403  sotritric  4427  sotritrieq  4428  seeq1  4442  seeq2  4443  alxfr  4564  ralxfrd  4565  rexxfrd  4566  ordelsuc  4609  sosng  4805  iss  5065  iotaval  5305  funeq  5353  funssres  5376  f0dom0  5539  tz6.12c  5678  fnbrfvb  5693  ssimaex  5716  fvimacnv  5771  elpreima  5775  fsn  5827  fconst2g  5877  fndmexb  5885  elunirn  5917  f1ocnvfvb  5931  foeqcnvco  5941  f1eqcocnv  5942  fliftfun  5947  isose  5972  isopo  5974  isoso  5976  f1oiso2  5978  eusvobj2  6014  oprabid  6060  f1opw2  6239  op1steq  6351  fvn0elsuppb  6430  rntpos  6466  frecabcl  6608  nnsucelsuc  6702  nnsucsssuc  6703  nnsseleq  6712  nnaord  6720  nnmord  6728  nnaordex  6739  nnawordex  6740  nnm00  6741  erexb  6770  swoord1  6774  swoord2  6775  iinerm  6819  fundmen  7024  dom1o  7045  mapxpen  7077  ssenen  7080  nneneq  7086  nndomo  7093  fidifsnen  7100  en1eqsnbi  7191  suplub2ti  7260  isoti  7266  ordiso2  7294  ordiso  7295  ctm  7368  ctssdc  7372  enomni  7398  enmkv  7421  enwomni  7429  pm54.43  7455  pr2ne  7457  ltexnqq  7688  genprndl  7801  genprndu  7802  nqprl  7831  nqpru  7832  1idprl  7870  1idpru  7871  ltexprlemrnd  7885  ltaprg  7899  recexprlemrnd  7909  cauappcvgprlemrnd  7930  caucvgprlemrnd  7953  caucvgprprlemrnd  7981  suplocexprlemrl  7997  suplocexprlemru  7999  map2psrprg  8085  ltxrlt  8304  lttri3  8318  addlsub  8608  addid0  8611  ltadd2  8658  eqord1  8722  reapti  8818  apreap  8826  ltmul1  8831  apreim  8842  ltleap  8871  mulap0b  8894  recapb  8910  apmul1  9027  rerecapb  9082  lt2msq  9125  nnsub  9241  zltnle  9586  zleloe  9587  zrevaddcl  9591  zltp1le  9595  zapne  9615  nn0n0n1ge2b  9620  zdiv  9629  nneo  9644  zeo2  9647  qrevaddcl  9939  npnflt  10111  nmnfgt  10114  xltneg  10132  xleadd1  10171  iccid  10221  zltaddlt1le  10304  fzn  10339  0fz1  10342  uzsplit  10389  fzm1  10397  fzrevral  10402  ssfzo12bi  10533  qltnle  10566  ioo0  10582  ioom  10583  ico0  10584  ioc0  10585  flqge  10605  modqid2  10676  modqmuladd  10691  frec2uzlt2d  10729  seqf1oglem1  10844  qsqeqor  10975  nn0ltexp2  11034  hashtpg  11174  len0nnbi  11214  ccats1pfxeqbi  11389  reuccatpfxs1  11394  shftlem  11456  shftuz  11457  caucvgrelemcau  11620  sqrtsq  11684  abs00ap  11702  cau3lem  11754  maxleb  11856  rexico  11861  negfi  11868  climshft  11944  zsumdc  12025  fsum3  12028  fsum00  12103  zproddc  12220  fprodseq  12224  dvdsval2  12431  moddvds  12440  negdvdsb  12448  dvdsnegb  12449  dvdscmulr  12461  dvdsmulcr  12462  dvdssub2  12476  fzo0dvdseq  12498  ltoddhalfle  12534  dvdsgcdb  12664  gcdzeq  12673  dvdssqlem  12681  lcmeq0  12723  lcmdvdsb  12736  coprmgcdb  12740  ncoprmgcdne1b  12741  cncongr  12757  isprm2lem  12768  dvdsprime  12774  dvdsprm  12789  coprm  12796  euclemma  12798  rpexp  12805  prmdiveq  12888  hashgcdlem  12890  odzdvds  12898  pythagtrip  12936  pcdvdsb  12973  pc2dvds  12983  pcprmpw2  12986  pcprmpw  12987  enct  13134  intopsn  13530  gsumfzval  13554  isgrpid2  13703  isgrpinv  13717  f1ghm0to0  13939  ringinvnz1ne0  14143  ringinvnzdiv  14144  unitmulclb  14209  dvreq1  14237  isnzr2  14279  rrgeq0  14360  domneq0  14368  lssats2  14510  lspsneq0  14522  znunit  14755  toponcomb  14839  tgss3  14889  isopn3  14936  neiint  14956  neipsm  14965  opnneissb  14966  opnssneib  14967  tpnei  14971  opnneiid  14975  restopnb  14992  tgcn  15019  tgcnp  15020  iscnp4  15029  cnpnei  15030  cnntr  15036  lmss  15057  upxp  15083  txcn  15086  txlm  15090  hmeoopn  15122  hmeocld  15123  xblm  15228  blssexps  15240  blssex  15241  isxms2  15263  neibl  15302  metss  15305  metrest  15317  metcnp3  15322  ivthinclemlr  15448  ivthinclemur  15450  cnplimccntop  15481  eflt  15586  dvdsppwf1o  15803  lgsdir2lem4  15850  lgsne0  15857  gausslemma2dlem1a  15877  lgsquadlem1  15896  m1lgs  15904  uhgr0vb  16025  ausgrusgrben  16109  ushgredgedg  16167  ushgredgedgloop  16169  usgr0vb  16174  loopclwwlkn1b  16360  eupth2lem3lem4fi  16414  bj-charfunbi  16527  subctctexmid  16722  triap  16761  iswomni0  16784