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  5868  elunirn  5906  f1ocnvfvb  5920  foeqcnvco  5930  f1eqcocnv  5931  fliftfun  5936  isose  5961  isopo  5963  isoso  5965  f1oiso2  5967  eusvobj2  6003  oprabid  6049  f1opw2  6228  op1steq  6341  rntpos  6422  frecabcl  6564  nnsucelsuc  6658  nnsucsssuc  6659  nnsseleq  6668  nnaord  6676  nnmord  6684  nnaordex  6695  nnawordex  6696  nnm00  6697  erexb  6726  swoord1  6730  swoord2  6731  iinerm  6775  fundmen  6980  dom1o  7001  mapxpen  7033  ssenen  7036  nneneq  7042  nndomo  7049  fidifsnen  7056  en1eqsnbi  7147  suplub2ti  7199  isoti  7205  ordiso2  7233  ordiso  7234  ctm  7307  ctssdc  7311  enomni  7337  enmkv  7360  enwomni  7368  pm54.43  7394  pr2ne  7396  ltexnqq  7627  genprndl  7740  genprndu  7741  nqprl  7770  nqpru  7771  1idprl  7809  1idpru  7810  ltexprlemrnd  7824  ltaprg  7838  recexprlemrnd  7848  cauappcvgprlemrnd  7869  caucvgprlemrnd  7892  caucvgprprlemrnd  7920  suplocexprlemrl  7936  suplocexprlemru  7938  map2psrprg  8024  ltxrlt  8244  lttri3  8258  addlsub  8548  addid0  8551  ltadd2  8598  eqord1  8662  reapti  8758  apreap  8766  ltmul1  8771  apreim  8782  ltleap  8811  mulap0b  8834  recapb  8850  apmul1  8967  rerecapb  9022  lt2msq  9065  nnsub  9181  zltnle  9524  zleloe  9525  zrevaddcl  9529  zltp1le  9533  zapne  9553  nn0n0n1ge2b  9558  zdiv  9567  nneo  9582  zeo2  9585  qrevaddcl  9877  npnflt  10049  nmnfgt  10052  xltneg  10070  xleadd1  10109  iccid  10159  zltaddlt1le  10241  fzn  10276  0fz1  10279  uzsplit  10326  fzm1  10334  fzrevral  10339  ssfzo12bi  10469  qltnle  10502  ioo0  10518  ioom  10519  ico0  10520  ioc0  10521  flqge  10541  modqid2  10612  modqmuladd  10627  frec2uzlt2d  10665  seqf1oglem1  10780  qsqeqor  10911  nn0ltexp2  10970  len0nnbi  11147  ccats1pfxeqbi  11322  reuccatpfxs1  11327  shftlem  11376  shftuz  11377  caucvgrelemcau  11540  sqrtsq  11604  abs00ap  11622  cau3lem  11674  maxleb  11776  rexico  11781  negfi  11788  climshft  11864  zsumdc  11944  fsum3  11947  fsum00  12022  zproddc  12139  fprodseq  12143  dvdsval2  12350  moddvds  12359  negdvdsb  12367  dvdsnegb  12368  dvdscmulr  12380  dvdsmulcr  12381  dvdssub2  12395  fzo0dvdseq  12417  ltoddhalfle  12453  dvdsgcdb  12583  gcdzeq  12592  dvdssqlem  12600  lcmeq0  12642  lcmdvdsb  12655  coprmgcdb  12659  ncoprmgcdne1b  12660  cncongr  12676  isprm2lem  12687  dvdsprime  12693  dvdsprm  12708  coprm  12715  euclemma  12717  rpexp  12724  prmdiveq  12807  hashgcdlem  12809  odzdvds  12817  pythagtrip  12855  pcdvdsb  12892  pc2dvds  12902  pcprmpw2  12905  pcprmpw  12906  enct  13053  intopsn  13449  gsumfzval  13473  isgrpid2  13622  isgrpinv  13636  f1ghm0to0  13858  ringinvnz1ne0  14061  ringinvnzdiv  14062  unitmulclb  14127  dvreq1  14155  isnzr2  14197  rrgeq0  14278  domneq0  14285  lssats2  14427  lspsneq0  14439  znunit  14672  toponcomb  14751  tgss3  14801  isopn3  14848  neiint  14868  neipsm  14877  opnneissb  14878  opnssneib  14879  tpnei  14883  opnneiid  14887  restopnb  14904  tgcn  14931  tgcnp  14932  iscnp4  14941  cnpnei  14942  cnntr  14948  lmss  14969  upxp  14995  txcn  14998  txlm  15002  hmeoopn  15034  hmeocld  15035  xblm  15140  blssexps  15152  blssex  15153  isxms2  15175  neibl  15214  metss  15217  metrest  15229  metcnp3  15234  ivthinclemlr  15360  ivthinclemur  15362  cnplimccntop  15393  eflt  15498  dvdsppwf1o  15712  lgsdir2lem4  15759  lgsne0  15766  gausslemma2dlem1a  15786  lgsquadlem1  15805  m1lgs  15813  uhgr0vb  15934  ausgrusgrben  16018  ushgredgedg  16076  ushgredgedgloop  16078  usgr0vb  16083  loopclwwlkn1b  16269  bj-charfunbi  16406  subctctexmid  16601  triap  16633  iswomni0  16655