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  596  notbi  668  pm5.21  697  nbn2  699  2falsed  704  pm5.21ndd  707  oibabs  716  orbi2d  792  con4biddc  859  con1bidc  876  con1bdc  880  dedlema  972  dedlemb  973  xorbin  1404  albi  1491  19.21ht  1604  exbi  1627  19.23t  1700  equequ1  1735  equequ2  1736  equsexd  1752  dral1  1753  cbv2h  1771  cbv2w  1773  sbequ12  1794  sbiedh  1810  drex1  1821  ax11b  1849  sbequ  1863  sbft  1871  sb56  1909  cbvexdh  1950  eupickb  2135  eupickbi  2136  elequ1  2180  elequ2  2181  ceqsalt  2798  ceqex  2900  mob2  2953  euxfr2dc  2958  reu6  2962  sbciegft  3029  csbiebt  3133  sseq1  3216  reupick  3457  reupick2  3459  disjeq2  4025  disjeq1  4028  exmidsssnc  4248  copsexg  4289  euotd  4300  poeq2  4348  sotritric  4372  sotritrieq  4373  seeq1  4387  seeq2  4388  alxfr  4509  ralxfrd  4510  rexxfrd  4511  ordelsuc  4554  sosng  4749  iss  5006  iotaval  5244  funeq  5292  funssres  5314  f0dom0  5471  tz6.12c  5608  fnbrfvb  5621  ssimaex  5642  fvimacnv  5697  elpreima  5701  fsn  5754  fconst2g  5801  elunirn  5837  f1ocnvfvb  5851  foeqcnvco  5861  f1eqcocnv  5862  fliftfun  5867  isose  5892  isopo  5894  isoso  5896  f1oiso2  5898  eusvobj2  5932  oprabid  5978  f1opw2  6154  op1steq  6267  rntpos  6345  frecabcl  6487  nnsucelsuc  6579  nnsucsssuc  6580  nnsseleq  6589  nnaord  6597  nnmord  6605  nnaordex  6616  nnawordex  6617  nnm00  6618  erexb  6647  swoord1  6651  swoord2  6652  iinerm  6696  fundmen  6900  mapxpen  6947  ssenen  6950  nneneq  6956  nndomo  6963  fidifsnen  6969  en1eqsnbi  7053  suplub2ti  7105  isoti  7111  ordiso2  7139  ordiso  7140  ctm  7213  ctssdc  7217  enomni  7243  enmkv  7266  enwomni  7274  pm54.43  7300  pr2ne  7302  ltexnqq  7523  genprndl  7636  genprndu  7637  nqprl  7666  nqpru  7667  1idprl  7705  1idpru  7706  ltexprlemrnd  7720  ltaprg  7734  recexprlemrnd  7744  cauappcvgprlemrnd  7765  caucvgprlemrnd  7788  caucvgprprlemrnd  7816  suplocexprlemrl  7832  suplocexprlemru  7834  map2psrprg  7920  ltxrlt  8140  lttri3  8154  addlsub  8444  addid0  8447  ltadd2  8494  eqord1  8558  reapti  8654  apreap  8662  ltmul1  8667  apreim  8678  ltleap  8707  mulap0b  8730  recapb  8746  apmul1  8863  rerecapb  8918  lt2msq  8961  nnsub  9077  zltnle  9420  zleloe  9421  zrevaddcl  9425  zltp1le  9429  zapne  9449  nn0n0n1ge2b  9454  zdiv  9463  nneo  9478  zeo2  9481  qrevaddcl  9767  npnflt  9939  nmnfgt  9942  xltneg  9960  xleadd1  9999  iccid  10049  zltaddlt1le  10131  fzn  10166  0fz1  10169  uzsplit  10216  fzm1  10224  fzrevral  10229  ssfzo12bi  10356  qltnle  10388  ioo0  10404  ioom  10405  ico0  10406  ioc0  10407  flqge  10427  modqid2  10498  modqmuladd  10513  frec2uzlt2d  10551  seqf1oglem1  10666  qsqeqor  10797  nn0ltexp2  10856  len0nnbi  11030  shftlem  11160  shftuz  11161  caucvgrelemcau  11324  sqrtsq  11388  abs00ap  11406  cau3lem  11458  maxleb  11560  rexico  11565  negfi  11572  climshft  11648  zsumdc  11728  fsum3  11731  fsum00  11806  zproddc  11923  fprodseq  11927  dvdsval2  12134  moddvds  12143  negdvdsb  12151  dvdsnegb  12152  dvdscmulr  12164  dvdsmulcr  12165  dvdssub2  12179  fzo0dvdseq  12201  ltoddhalfle  12237  dvdsgcdb  12367  gcdzeq  12376  dvdssqlem  12384  lcmeq0  12426  lcmdvdsb  12439  coprmgcdb  12443  ncoprmgcdne1b  12444  cncongr  12460  isprm2lem  12471  dvdsprime  12477  dvdsprm  12492  coprm  12499  euclemma  12501  rpexp  12508  prmdiveq  12591  hashgcdlem  12593  odzdvds  12601  pythagtrip  12639  pcdvdsb  12676  pc2dvds  12686  pcprmpw2  12689  pcprmpw  12690  enct  12837  intopsn  13232  gsumfzval  13256  isgrpid2  13405  isgrpinv  13419  f1ghm0to0  13641  ringinvnz1ne0  13844  ringinvnzdiv  13845  unitmulclb  13909  dvreq1  13937  isnzr2  13979  rrgeq0  14060  domneq0  14067  lssats2  14209  lspsneq0  14221  znunit  14454  toponcomb  14533  tgss3  14583  isopn3  14630  neiint  14650  neipsm  14659  opnneissb  14660  opnssneib  14661  tpnei  14665  opnneiid  14669  restopnb  14686  tgcn  14713  tgcnp  14714  iscnp4  14723  cnpnei  14724  cnntr  14730  lmss  14751  upxp  14777  txcn  14780  txlm  14784  hmeoopn  14816  hmeocld  14817  xblm  14922  blssexps  14934  blssex  14935  isxms2  14957  neibl  14996  metss  14999  metrest  15011  metcnp3  15016  ivthinclemlr  15142  ivthinclemur  15144  cnplimccntop  15175  eflt  15280  dvdsppwf1o  15494  lgsdir2lem4  15541  lgsne0  15548  gausslemma2dlem1a  15568  lgsquadlem1  15587  m1lgs  15595  bj-charfunbi  15784  subctctexmid  15974  triap  16005  iswomni0  16027