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  7243  isoti  7249  ordiso2  7277  ordiso  7278  ctm  7351  ctssdc  7355  enomni  7381  enmkv  7404  enwomni  7412  pm54.43  7438  pr2ne  7440  ltexnqq  7671  genprndl  7784  genprndu  7785  nqprl  7814  nqpru  7815  1idprl  7853  1idpru  7854  ltexprlemrnd  7868  ltaprg  7882  recexprlemrnd  7892  cauappcvgprlemrnd  7913  caucvgprlemrnd  7936  caucvgprprlemrnd  7964  suplocexprlemrl  7980  suplocexprlemru  7982  map2psrprg  8068  ltxrlt  8288  lttri3  8302  addlsub  8592  addid0  8595  ltadd2  8642  eqord1  8706  reapti  8802  apreap  8810  ltmul1  8815  apreim  8826  ltleap  8855  mulap0b  8878  recapb  8894  apmul1  9011  rerecapb  9066  lt2msq  9109  nnsub  9225  zltnle  9568  zleloe  9569  zrevaddcl  9573  zltp1le  9577  zapne  9597  nn0n0n1ge2b  9602  zdiv  9611  nneo  9626  zeo2  9629  qrevaddcl  9921  npnflt  10093  nmnfgt  10096  xltneg  10114  xleadd1  10153  iccid  10203  zltaddlt1le  10285  fzn  10320  0fz1  10323  uzsplit  10370  fzm1  10378  fzrevral  10383  ssfzo12bi  10514  qltnle  10547  ioo0  10563  ioom  10564  ico0  10565  ioc0  10566  flqge  10586  modqid2  10657  modqmuladd  10672  frec2uzlt2d  10710  seqf1oglem1  10825  qsqeqor  10956  nn0ltexp2  11015  hashtpg  11155  len0nnbi  11195  ccats1pfxeqbi  11370  reuccatpfxs1  11375  shftlem  11437  shftuz  11438  caucvgrelemcau  11601  sqrtsq  11665  abs00ap  11683  cau3lem  11735  maxleb  11837  rexico  11842  negfi  11849  climshft  11925  zsumdc  12006  fsum3  12009  fsum00  12084  zproddc  12201  fprodseq  12205  dvdsval2  12412  moddvds  12421  negdvdsb  12429  dvdsnegb  12430  dvdscmulr  12442  dvdsmulcr  12443  dvdssub2  12457  fzo0dvdseq  12479  ltoddhalfle  12515  dvdsgcdb  12645  gcdzeq  12654  dvdssqlem  12662  lcmeq0  12704  lcmdvdsb  12717  coprmgcdb  12721  ncoprmgcdne1b  12722  cncongr  12738  isprm2lem  12749  dvdsprime  12755  dvdsprm  12770  coprm  12777  euclemma  12779  rpexp  12786  prmdiveq  12869  hashgcdlem  12871  odzdvds  12879  pythagtrip  12917  pcdvdsb  12954  pc2dvds  12964  pcprmpw2  12967  pcprmpw  12968  enct  13115  intopsn  13511  gsumfzval  13535  isgrpid2  13684  isgrpinv  13698  f1ghm0to0  13920  ringinvnz1ne0  14124  ringinvnzdiv  14125  unitmulclb  14190  dvreq1  14218  isnzr2  14260  rrgeq0  14341  domneq0  14348  lssats2  14490  lspsneq0  14502  znunit  14735  toponcomb  14819  tgss3  14869  isopn3  14916  neiint  14936  neipsm  14945  opnneissb  14946  opnssneib  14947  tpnei  14951  opnneiid  14955  restopnb  14972  tgcn  14999  tgcnp  15000  iscnp4  15009  cnpnei  15010  cnntr  15016  lmss  15037  upxp  15063  txcn  15066  txlm  15070  hmeoopn  15102  hmeocld  15103  xblm  15208  blssexps  15220  blssex  15221  isxms2  15243  neibl  15282  metss  15285  metrest  15297  metcnp3  15302  ivthinclemlr  15428  ivthinclemur  15430  cnplimccntop  15461  eflt  15566  dvdsppwf1o  15783  lgsdir2lem4  15830  lgsne0  15837  gausslemma2dlem1a  15857  lgsquadlem1  15876  m1lgs  15884  uhgr0vb  16005  ausgrusgrben  16089  ushgredgedg  16147  ushgredgedgloop  16149  usgr0vb  16154  loopclwwlkn1b  16340  eupth2lem3lem4fi  16394  bj-charfunbi  16507  subctctexmid  16702  triap  16741  iswomni0  16764