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  703  nbn2  705  2falsed  710  pm5.21ndd  713  oibabs  722  orbi2d  798  con4biddc  865  con1bidc  882  con1bdc  886  dedlema  978  dedlemb  979  xorbin  1429  albi  1517  19.21ht  1630  exbi  1653  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1778  dral1  1779  cbv2h  1797  cbv2w  1799  sbequ12  1820  sbiedh  1836  drex1  1847  ax11b  1875  sbequ  1889  sbft  1897  sb56  1935  cbvexdh  1976  eupickb  2162  eupickbi  2163  elequ1  2207  elequ2  2208  ceqsalt  2840  ceqex  2944  mob2  2997  euxfr2dc  3002  reu6  3006  sbciegft  3073  csbiebt  3178  sseq1  3261  reupick  3505  reupick2  3507  disjeq2  4089  disjeq1  4092  exmidsssnc  4316  copsexg  4360  euotd  4371  poeq2  4421  sotritric  4445  sotritrieq  4446  seeq1  4460  seeq2  4461  alxfr  4582  ralxfrd  4583  rexxfrd  4584  ordelsuc  4627  sosng  4823  iss  5084  iotaval  5324  funeq  5372  funssres  5395  f0dom0  5561  tz6.12c  5700  fnbrfvb  5715  ssimaex  5738  fvimacnv  5793  elpreima  5797  fsn  5849  fconst2g  5899  fndmexb  5907  elunirn  5939  f1ocnvfvb  5953  foeqcnvco  5963  f1eqcocnv  5964  fliftfun  5969  isose  5994  isopo  5996  isoso  5998  f1oiso2  6000  eusvobj2  6036  oprabid  6082  f1opw2  6261  op1steq  6373  fvn0elsuppb  6452  rntpos  6488  frecabcl  6630  nnsucelsuc  6724  nnsucsssuc  6725  nnsseleq  6734  nnaord  6742  nnmord  6750  nnaordex  6761  nnawordex  6762  nnm00  6763  erexb  6792  swoord1  6796  swoord2  6797  iinerm  6841  mapsnd  6923  fundmen  7047  dom1o  7069  mapxpen  7101  mapunen  7104  ssenen  7105  nneneq  7111  nndomo  7118  fidifsnen  7125  en1eqsnbi  7219  suplub2ti  7292  isoti  7298  ordiso2  7326  ordiso  7327  ctm  7400  ctssdc  7404  enomni  7430  enmkv  7453  enwomni  7461  pm54.43  7487  pr2ne  7489  ltexnqq  7723  genprndl  7836  genprndu  7837  nqprl  7866  nqpru  7867  1idprl  7905  1idpru  7906  ltexprlemrnd  7920  ltaprg  7934  recexprlemrnd  7944  cauappcvgprlemrnd  7965  caucvgprlemrnd  7988  caucvgprprlemrnd  8016  suplocexprlemrl  8032  suplocexprlemru  8034  map2psrprg  8120  ltxrlt  8339  lttri3  8353  addlsub  8643  addid0  8646  ltadd2  8693  eqord1  8757  reapti  8853  apreap  8861  ltmul1  8866  apreim  8877  ltleap  8906  mulap0b  8929  recapb  8945  apmul1  9062  rerecapb  9117  lt2msq  9160  nnsub  9276  zltnle  9623  zleloe  9624  zrevaddcl  9628  zltp1le  9632  zapne  9652  nn0n0n1ge2b  9657  zdiv  9666  nneo  9681  zeo2  9684  qrevaddcl  9976  npnflt  10148  nmnfgt  10151  xltneg  10169  xleadd1  10208  iccid  10258  zltaddlt1le  10341  fzn  10376  0fz1  10379  uzsplit  10426  fzm1  10434  fzrevral  10439  ssfzo12bi  10570  qltnle  10603  ioo0  10619  ioom  10620  ico0  10621  ioc0  10622  flqge  10642  modqid2  10713  modqmuladd  10728  frec2uzlt2d  10766  seqf1oglem1  10881  qsqeqor  11012  nn0ltexp2  11071  hashtpg  11219  len0nnbi  11259  ccats1pfxeqbi  11434  reuccatpfxs1  11439  shftlem  11501  shftuz  11502  caucvgrelemcau  11665  sqrtsq  11729  abs00ap  11747  cau3lem  11799  maxleb  11901  rexico  11906  negfi  11913  climshft  11989  zsumdc  12070  fsum3  12073  fsum00  12148  zproddc  12265  fprodseq  12269  dvdsval2  12476  moddvds  12485  negdvdsb  12493  dvdsnegb  12494  dvdscmulr  12506  dvdsmulcr  12507  dvdssub2  12521  fzo0dvdseq  12543  ltoddhalfle  12579  dvdsgcdb  12709  gcdzeq  12718  dvdssqlem  12726  lcmeq0  12768  lcmdvdsb  12781  coprmgcdb  12785  ncoprmgcdne1b  12786  cncongr  12802  isprm2lem  12813  dvdsprime  12819  dvdsprm  12834  coprm  12841  euclemma  12843  rpexp  12850  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  pythagtrip  12981  pcdvdsb  13018  pc2dvds  13028  pcprmpw2  13031  pcprmpw  13032  enct  13184  intopsn  13580  gsumfzval  13604  isgrpid2  13753  isgrpinv  13767  f1ghm0to0  13989  ringinvnz1ne0  14193  ringinvnzdiv  14194  unitmulclb  14259  dvreq1  14287  isnzr2  14329  rrgeq0  14410  domneq0  14418  lssats2  14562  lspsneq0  14574  znunit  14807  toponcomb  14893  tgss3  14943  isopn3  14990  neiint  15010  neipsm  15019  opnneissb  15020  opnssneib  15021  tpnei  15025  opnneiid  15029  restopnb  15046  tgcn  15073  tgcnp  15074  iscnp4  15083  cnpnei  15084  cnntr  15090  lmss  15111  upxp  15137  txcn  15140  txlm  15144  hmeoopn  15176  hmeocld  15177  xblm  15282  blssexps  15294  blssex  15295  isxms2  15317  neibl  15356  metss  15359  metrest  15371  metcnp3  15376  ivthinclemlr  15502  ivthinclemur  15504  cnplimccntop  15535  eflt  15640  dvdsppwf1o  15857  lgsdir2lem4  15904  lgsne0  15911  gausslemma2dlem1a  15931  lgsquadlem1  15950  m1lgs  15958  uhgr0vb  16079  ausgrusgrben  16163  ushgredgedg  16221  ushgredgedgloop  16223  usgr0vb  16228  loopclwwlkn1b  16414  eupth2lem3lem4fi  16468  bj-charfunbi  16581  subctctexmid  16774  triap  16813  iswomni0  16836