Theorem impbid 120

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

Syntax hints:   → wi 4   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicom1  122  impbid1  130  pm5.74  168  imbi1d  220  pm5.501  233  pm5.32d  423  impbida  528  notbid  592  pm5.21  611  nbn2  613  2falsed  618  pm5.21ndd  621  orbi2d  704  con4biddc  754  con1bidc  768  con1bdc  772  oibabs  800  dedlema  876  dedlemb  877  xorbin  1275  albi  1357  19.21ht  1473  exbi  1495  19.23t  1567  equequ1  1598  equequ2  1599  elequ1  1600  elequ2  1601  equsexd  1617  dral1  1618  cbv2h  1634  sbequ12  1654  sbiedh  1670  drex1  1679  ax11b  1707  sbequ  1721  sbft  1728  sb56  1765  cbvexdh  1801  eupickb  1981  eupickbi  1982  ceqsalt  2580  ceqex  2671  mob2  2721  euxfr2dc  2726  reu6  2730  sbciegft  2793  eqsbc3r  2819  csbiebt  2886  sseq1  2966  reupick  3221  reupick2  3223  disjeq2  3749  disjeq1  3752  copsexg  3981  euotd  3991  poeq2  4037  sotritric  4061  sotritrieq  4062  seeq1  4076  seeq2  4077  alxfr  4193  ralxfrd  4194  rexxfrd  4195  ordelsuc  4231  sosng  4413  iss  4654  iotaval  4878  funeq  4921  funssres  4942  tz6.12c  5203  fnbrfvb  5214  ssimaex  5234  fvimacnv  5282  elpreima  5286  fsn  5335  fconst2g  5376  elunirn  5405  f1ocnvfvb  5420  foeqcnvco  5430  f1eqcocnv  5431  fliftfun  5436  isose  5460  isopo  5462  isoso  5464  f1oiso2  5466  eusvobj2  5498  oprabid  5537  f1opw2  5706  op1steq  5805  rntpos  5872  nnsucelsuc  6070  nnsucsssuc  6071  nnsseleq  6079  nnaord  6082  nnmord  6090  nnaordex  6100  nnawordex  6101  nnm00  6102  erexb  6131  swoord1  6135  swoord2  6136  iinerm  6178  fundmen  6286  nneneq  6320  nndomo  6326  fidifsnen  6331  ordiso2  6357  ordiso  6358  ltexnqq  6506  genprndl  6619  genprndu  6620  nqprl  6649  nqpru  6650  1idprl  6688  1idpru  6689  ltexprlemrnd  6703  ltaprg  6717  recexprlemrnd  6727  cauappcvgprlemrnd  6748  caucvgprlemrnd  6771  caucvgprprlemrnd  6799  ltxrlt  7085  lttri3  7098  ltadd2  7416  reapti  7570  apreap  7578  ltmul1  7583  apreim  7594  ltleap  7621  mulap0b  7636  apmul1  7764  lt2msq  7852  nnsub  7952  zltnle  8291  zleloe  8292  zrevaddcl  8295  zltp1le  8298  zapne  8315  nn0n0n1ge2b  8320  zdiv  8328  nneo  8341  zeo2  8344  qrevaddcl  8578  xltneg  8749  iccid  8794  fzn  8906  0fz1  8909  uzsplit  8954  fzm1  8962  fzrevral  8967  ssfzo12bi  9081  qltnle  9101  flqge  9124  frec2uzlt2d  9190  shftlem  9417  shftuz  9418  caucvgrelemcau  9579  sqrtsq  9642  abs00ap  9660  cau3lem  9710  climshft  9825  bj-notbi  10045