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  702  nbn2  704  2falsed  709  pm5.21ndd  712  oibabs  721  orbi2d  797  con4biddc  864  con1bidc  881  con1bdc  885  dedlema  977  dedlemb  978  xorbin  1428  albi  1516  19.21ht  1629  exbi  1652  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  2829  ceqex  2933  mob2  2986  euxfr2dc  2991  reu6  2995  sbciegft  3062  csbiebt  3167  sseq1  3250  reupick  3491  reupick2  3493  disjeq2  4068  disjeq1  4071  exmidsssnc  4293  copsexg  4336  euotd  4347  poeq2  4397  sotritric  4421  sotritrieq  4422  seeq1  4436  seeq2  4437  alxfr  4558  ralxfrd  4559  rexxfrd  4560  ordelsuc  4603  sosng  4799  iss  5059  iotaval  5298  funeq  5346  funssres  5369  f0dom0  5530  tz6.12c  5669  fnbrfvb  5684  ssimaex  5707  fvimacnv  5762  elpreima  5766  fsn  5819  fconst2g  5869  elunirn  5907  f1ocnvfvb  5921  foeqcnvco  5931  f1eqcocnv  5932  fliftfun  5937  isose  5962  isopo  5964  isoso  5966  f1oiso2  5968  eusvobj2  6004  oprabid  6050  f1opw2  6229  op1steq  6342  rntpos  6423  frecabcl  6565  nnsucelsuc  6659  nnsucsssuc  6660  nnsseleq  6669  nnaord  6677  nnmord  6685  nnaordex  6696  nnawordex  6697  nnm00  6698  erexb  6727  swoord1  6731  swoord2  6732  iinerm  6776  fundmen  6981  dom1o  7002  mapxpen  7034  ssenen  7037  nneneq  7043  nndomo  7050  fidifsnen  7057  en1eqsnbi  7148  suplub2ti  7200  isoti  7206  ordiso2  7234  ordiso  7235  ctm  7308  ctssdc  7312  enomni  7338  enmkv  7361  enwomni  7369  pm54.43  7395  pr2ne  7397  ltexnqq  7628  genprndl  7741  genprndu  7742  nqprl  7771  nqpru  7772  1idprl  7810  1idpru  7811  ltexprlemrnd  7825  ltaprg  7839  recexprlemrnd  7849  cauappcvgprlemrnd  7870  caucvgprlemrnd  7893  caucvgprprlemrnd  7921  suplocexprlemrl  7937  suplocexprlemru  7939  map2psrprg  8025  ltxrlt  8245  lttri3  8259  addlsub  8549  addid0  8552  ltadd2  8599  eqord1  8663  reapti  8759  apreap  8767  ltmul1  8772  apreim  8783  ltleap  8812  mulap0b  8835  recapb  8851  apmul1  8968  rerecapb  9023  lt2msq  9066  nnsub  9182  zltnle  9525  zleloe  9526  zrevaddcl  9530  zltp1le  9534  zapne  9554  nn0n0n1ge2b  9559  zdiv  9568  nneo  9583  zeo2  9586  qrevaddcl  9878  npnflt  10050  nmnfgt  10053  xltneg  10071  xleadd1  10110  iccid  10160  zltaddlt1le  10242  fzn  10277  0fz1  10280  uzsplit  10327  fzm1  10335  fzrevral  10340  ssfzo12bi  10471  qltnle  10504  ioo0  10520  ioom  10521  ico0  10522  ioc0  10523  flqge  10543  modqid2  10614  modqmuladd  10629  frec2uzlt2d  10667  seqf1oglem1  10782  qsqeqor  10913  nn0ltexp2  10972  hashtpg  11112  len0nnbi  11152  ccats1pfxeqbi  11327  reuccatpfxs1  11332  shftlem  11394  shftuz  11395  caucvgrelemcau  11558  sqrtsq  11622  abs00ap  11640  cau3lem  11692  maxleb  11794  rexico  11799  negfi  11806  climshft  11882  zsumdc  11963  fsum3  11966  fsum00  12041  zproddc  12158  fprodseq  12162  dvdsval2  12369  moddvds  12378  negdvdsb  12386  dvdsnegb  12387  dvdscmulr  12399  dvdsmulcr  12400  dvdssub2  12414  fzo0dvdseq  12436  ltoddhalfle  12472  dvdsgcdb  12602  gcdzeq  12611  dvdssqlem  12619  lcmeq0  12661  lcmdvdsb  12674  coprmgcdb  12678  ncoprmgcdne1b  12679  cncongr  12695  isprm2lem  12706  dvdsprime  12712  dvdsprm  12727  coprm  12734  euclemma  12736  rpexp  12743  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  pythagtrip  12874  pcdvdsb  12911  pc2dvds  12921  pcprmpw2  12924  pcprmpw  12925  enct  13072  intopsn  13468  gsumfzval  13492  isgrpid2  13641  isgrpinv  13655  f1ghm0to0  13877  ringinvnz1ne0  14081  ringinvnzdiv  14082  unitmulclb  14147  dvreq1  14175  isnzr2  14217  rrgeq0  14298  domneq0  14305  lssats2  14447  lspsneq0  14459  znunit  14692  toponcomb  14771  tgss3  14821  isopn3  14868  neiint  14888  neipsm  14897  opnneissb  14898  opnssneib  14899  tpnei  14903  opnneiid  14907  restopnb  14924  tgcn  14951  tgcnp  14952  iscnp4  14961  cnpnei  14962  cnntr  14968  lmss  14989  upxp  15015  txcn  15018  txlm  15022  hmeoopn  15054  hmeocld  15055  xblm  15160  blssexps  15172  blssex  15173  isxms2  15195  neibl  15234  metss  15237  metrest  15249  metcnp3  15254  ivthinclemlr  15380  ivthinclemur  15382  cnplimccntop  15413  eflt  15518  dvdsppwf1o  15732  lgsdir2lem4  15779  lgsne0  15786  gausslemma2dlem1a  15806  lgsquadlem1  15825  m1lgs  15833  uhgr0vb  15954  ausgrusgrben  16038  ushgredgedg  16096  ushgredgedgloop  16098  usgr0vb  16103  loopclwwlkn1b  16289  eupth2lem3lem4fi  16343  bj-charfunbi  16457  subctctexmid  16652  triap  16684  iswomni0  16707