Theorem impbid 127

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicom1  129  impbid1  140  pm5.74  177  imbi1d  229  pm5.501  242  pm5.32d  437  impbida  560  notbid  624  pm5.21  643  nbn2  645  2falsed  650  pm5.21ndd  653  orbi2d  736  con4biddc  787  con1bidc  801  con1bdc  805  oibabs  833  dedlema  910  dedlemb  911  xorbin  1315  albi  1397  19.21ht  1513  exbi  1535  19.23t  1607  equequ1  1638  equequ2  1639  elequ1  1640  elequ2  1641  equsexd  1657  dral1  1658  cbv2h  1674  sbequ12  1694  sbiedh  1710  drex1  1719  ax11b  1747  sbequ  1761  sbft  1769  sb56  1806  cbvexdh  1842  eupickb  2022  eupickbi  2023  ceqsalt  2625  ceqex  2722  mob2  2772  euxfr2dc  2777  reu6  2781  sbciegft  2844  csbiebt  2942  sseq1  3020  reupick  3248  reupick2  3250  disjeq2  3770  disjeq1  3773  copsexg  3999  euotd  4009  poeq2  4055  sotritric  4079  sotritrieq  4080  seeq1  4094  seeq2  4095  alxfr  4211  ralxfrd  4212  rexxfrd  4213  ordelsuc  4249  sosng  4431  iss  4674  iotaval  4898  funeq  4941  funssres  4962  tz6.12c  5224  fnbrfvb  5235  ssimaex  5255  fvimacnv  5303  elpreima  5307  fsn  5356  fconst2g  5397  elunirn  5426  f1ocnvfvb  5440  foeqcnvco  5450  f1eqcocnv  5451  fliftfun  5456  isose  5480  isopo  5482  isoso  5484  f1oiso2  5486  eusvobj2  5518  oprabid  5557  f1opw2  5726  op1steq  5825  rntpos  5895  nnsucelsuc  6093  nnsucsssuc  6094  nnsseleq  6102  nnaord  6105  nnmord  6113  nnaordex  6123  nnawordex  6124  nnm00  6125  erexb  6154  swoord1  6158  swoord2  6159  iinerm  6201  fundmen  6309  nneneq  6343  nndomo  6350  fidifsnen  6355  suplub2ti  6414  isoti  6420  ordiso2  6446  ordiso  6447  pm54.43  6459  pr2ne  6461  ltexnqq  6598  genprndl  6711  genprndu  6712  nqprl  6741  nqpru  6742  1idprl  6780  1idpru  6781  ltexprlemrnd  6795  ltaprg  6809  recexprlemrnd  6819  cauappcvgprlemrnd  6840  caucvgprlemrnd  6863  caucvgprprlemrnd  6891  ltxrlt  7178  lttri3  7191  addlsub  7474  addid0  7477  ltadd2  7523  reapti  7679  apreap  7687  ltmul1  7692  apreim  7703  ltleap  7730  mulap0b  7745  apmul1  7876  lt2msq  7964  nnsub  8077  zltnle  8397  zleloe  8398  zrevaddcl  8401  zltp1le  8405  zapne  8422  nn0n0n1ge2b  8427  zdiv  8435  nneo  8450  zeo2  8453  qrevaddcl  8729  xltneg  8903  iccid  8948  zltaddlt1le  9028  fzn  9061  0fz1  9064  uzsplit  9109  fzm1  9117  fzrevral  9122  ssfzo12bi  9234  qltnle  9255  ioo0  9268  ioom  9269  ico0  9270  ioc0  9271  flqge  9284  modqid2  9353  modqmuladd  9368  frec2uzlt2d  9406  shftlem  9704  shftuz  9705  caucvgrelemcau  9866  sqrtsq  9930  abs00ap  9948  cau3lem  10000  maxleb  10102  rexico  10107  negfi  10110  climshft  10143  dvdsval2  10198  moddvds  10204  negdvdsb  10211  dvdsnegb  10212  dvdscmulr  10224  dvdsmulcr  10225  dvdssub2  10237  fzo0dvdseq  10257  ltoddhalfle  10293  dvdsgcdb  10402  gcdzeq  10411  dvdssqlem  10419  lcmeq0  10453  lcmdvdsb  10466  coprmgcdb  10470  ncoprmgcdne1b  10471  cncongr  10487  isprm2lem  10498  dvdsprime  10504  dvdsprm  10518  coprm  10523  euclemma  10525  rpexp  10532  bj-notbi  10716