Theorem impbid 128

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 127	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 49	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  441  impbida  566  notbid  633  pm5.21  652  nbn2  654  2falsed  659  pm5.21ndd  662  orbi2d  745  con4biddc  798  con1bidc  812  con1bdc  816  oibabs  844  dedlema  921  dedlemb  922  xorbin  1330  albi  1412  19.21ht  1528  exbi  1551  19.23t  1623  equequ1  1656  equequ2  1657  elequ1  1658  elequ2  1659  equsexd  1675  dral1  1676  cbv2h  1692  sbequ12  1712  sbiedh  1728  drex1  1737  ax11b  1765  sbequ  1779  sbft  1787  sb56  1824  cbvexdh  1861  eupickb  2041  eupickbi  2042  ceqsalt  2667  ceqex  2766  mob2  2817  euxfr2dc  2822  reu6  2826  sbciegft  2891  csbiebt  2989  sseq1  3070  reupick  3307  reupick2  3309  disjeq2  3856  disjeq1  3859  exmidsssnc  4064  copsexg  4104  euotd  4114  poeq2  4160  sotritric  4184  sotritrieq  4185  seeq1  4199  seeq2  4200  alxfr  4320  ralxfrd  4321  rexxfrd  4322  ordelsuc  4359  sosng  4550  iss  4801  iotaval  5035  funeq  5079  funssres  5101  f0dom0  5252  tz6.12c  5383  fnbrfvb  5394  ssimaex  5414  fvimacnv  5467  elpreima  5471  fsn  5524  fconst2g  5567  elunirn  5599  f1ocnvfvb  5613  foeqcnvco  5623  f1eqcocnv  5624  fliftfun  5629  isose  5654  isopo  5656  isoso  5658  f1oiso2  5660  eusvobj2  5692  oprabid  5735  f1opw2  5908  op1steq  6007  rntpos  6084  frecabcl  6226  nnsucelsuc  6317  nnsucsssuc  6318  nnsseleq  6327  nnaord  6335  nnmord  6343  nnaordex  6353  nnawordex  6354  nnm00  6355  erexb  6384  swoord1  6388  swoord2  6389  iinerm  6431  fundmen  6630  mapxpen  6671  ssenen  6674  nneneq  6680  nndomo  6687  fidifsnen  6693  en1eqsnbi  6765  suplub2ti  6803  isoti  6809  ordiso2  6835  ordiso  6836  ctm  6909  ctssdc  6912  enomni  6923  pm54.43  6957  pr2ne  6959  ltexnqq  7117  genprndl  7230  genprndu  7231  nqprl  7260  nqpru  7261  1idprl  7299  1idpru  7300  ltexprlemrnd  7314  ltaprg  7328  recexprlemrnd  7338  cauappcvgprlemrnd  7359  caucvgprlemrnd  7382  caucvgprprlemrnd  7410  ltxrlt  7702  lttri3  7715  addlsub  7999  addid0  8002  ltadd2  8048  eqord1  8112  reapti  8207  apreap  8215  ltmul1  8220  apreim  8231  ltleap  8259  mulap0b  8277  apmul1  8409  lt2msq  8502  nnsub  8617  zltnle  8952  zleloe  8953  zrevaddcl  8956  zltp1le  8960  zapne  8977  nn0n0n1ge2b  8982  zdiv  8991  nneo  9006  zeo2  9009  qrevaddcl  9286  npnflt  9439  nmnfgt  9442  xltneg  9460  xleadd1  9499  iccid  9549  zltaddlt1le  9630  fzn  9663  0fz1  9666  uzsplit  9713  fzm1  9721  fzrevral  9726  ssfzo12bi  9843  qltnle  9864  ioo0  9878  ioom  9879  ico0  9880  ioc0  9881  flqge  9896  modqid2  9965  modqmuladd  9980  frec2uzlt2d  10018  shftlem  10429  shftuz  10430  caucvgrelemcau  10592  sqrtsq  10656  abs00ap  10674  cau3lem  10726  maxleb  10828  rexico  10833  negfi  10838  climshft  10912  zsumdc  10992  fsum3  10995  fsum00  11070  dvdsval2  11291  moddvds  11297  negdvdsb  11304  dvdsnegb  11305  dvdscmulr  11317  dvdsmulcr  11318  dvdssub2  11330  fzo0dvdseq  11350  ltoddhalfle  11385  dvdsgcdb  11494  gcdzeq  11503  dvdssqlem  11511  lcmeq0  11545  lcmdvdsb  11558  coprmgcdb  11562  ncoprmgcdne1b  11563  cncongr  11579  isprm2lem  11590  dvdsprime  11596  dvdsprm  11610  coprm  11615  euclemma  11617  rpexp  11624  hashgcdlem  11695  toponcomb  11977  tgss3  12029  isopn3  12076  neiint  12096  neipsm  12105  opnneissb  12106  opnssneib  12107  tpnei  12111  opnneiid  12115  restopnb  12132  tgcn  12158  tgcnp  12159  iscnp4  12168  cnpnei  12169  cnntr  12175  lmss  12196  upxp  12222  txcn  12225  txlm  12229  xblm  12345  blssexps  12357  blssex  12358  isxms2  12380  neibl  12419  metss  12422  metrest  12434  metcnp3  12435  bj-notbi  12704  triap  12808