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  666  pm5.21  695  nbn2  697  2falsed  702  pm5.21ndd  705  oibabs  714  orbi2d  790  con4biddc  857  con1bidc  874  con1bdc  878  dedlema  969  dedlemb  970  xorbin  1384  albi  1468  19.21ht  1581  exbi  1604  19.23t  1677  equequ1  1712  equequ2  1713  equsexd  1729  dral1  1730  cbv2h  1748  cbv2w  1750  sbequ12  1771  sbiedh  1787  drex1  1798  ax11b  1826  sbequ  1840  sbft  1848  sb56  1885  cbvexdh  1926  eupickb  2107  eupickbi  2108  elequ1  2152  elequ2  2153  ceqsalt  2765  ceqex  2866  mob2  2919  euxfr2dc  2924  reu6  2928  sbciegft  2995  csbiebt  3098  sseq1  3180  reupick  3421  reupick2  3423  disjeq2  3986  disjeq1  3989  exmidsssnc  4205  copsexg  4246  euotd  4256  poeq2  4302  sotritric  4326  sotritrieq  4327  seeq1  4341  seeq2  4342  alxfr  4463  ralxfrd  4464  rexxfrd  4465  ordelsuc  4506  sosng  4701  iss  4955  iotaval  5191  funeq  5238  funssres  5260  f0dom0  5411  tz6.12c  5547  fnbrfvb  5558  ssimaex  5579  fvimacnv  5633  elpreima  5637  fsn  5690  fconst2g  5733  elunirn  5769  f1ocnvfvb  5783  foeqcnvco  5793  f1eqcocnv  5794  fliftfun  5799  isose  5824  isopo  5826  isoso  5828  f1oiso2  5830  eusvobj2  5863  oprabid  5909  f1opw2  6079  op1steq  6182  rntpos  6260  frecabcl  6402  nnsucelsuc  6494  nnsucsssuc  6495  nnsseleq  6504  nnaord  6512  nnmord  6520  nnaordex  6531  nnawordex  6532  nnm00  6533  erexb  6562  swoord1  6566  swoord2  6567  iinerm  6609  fundmen  6808  mapxpen  6850  ssenen  6853  nneneq  6859  nndomo  6866  fidifsnen  6872  en1eqsnbi  6950  suplub2ti  7002  isoti  7008  ordiso2  7036  ordiso  7037  ctm  7110  ctssdc  7114  enomni  7139  enmkv  7162  enwomni  7170  pm54.43  7191  pr2ne  7193  ltexnqq  7409  genprndl  7522  genprndu  7523  nqprl  7552  nqpru  7553  1idprl  7591  1idpru  7592  ltexprlemrnd  7606  ltaprg  7620  recexprlemrnd  7630  cauappcvgprlemrnd  7651  caucvgprlemrnd  7674  caucvgprprlemrnd  7702  suplocexprlemrl  7718  suplocexprlemru  7720  map2psrprg  7806  ltxrlt  8025  lttri3  8039  addlsub  8329  addid0  8332  ltadd2  8378  eqord1  8442  reapti  8538  apreap  8546  ltmul1  8551  apreim  8562  ltleap  8591  mulap0b  8614  recapb  8630  apmul1  8747  rerecapb  8802  lt2msq  8845  nnsub  8960  zltnle  9301  zleloe  9302  zrevaddcl  9305  zltp1le  9309  zapne  9329  nn0n0n1ge2b  9334  zdiv  9343  nneo  9358  zeo2  9361  qrevaddcl  9646  npnflt  9817  nmnfgt  9820  xltneg  9838  xleadd1  9877  iccid  9927  zltaddlt1le  10009  fzn  10044  0fz1  10047  uzsplit  10094  fzm1  10102  fzrevral  10107  ssfzo12bi  10227  qltnle  10248  ioo0  10262  ioom  10263  ico0  10264  ioc0  10265  flqge  10284  modqid2  10353  modqmuladd  10368  frec2uzlt2d  10406  qsqeqor  10633  nn0ltexp2  10691  shftlem  10827  shftuz  10828  caucvgrelemcau  10991  sqrtsq  11055  abs00ap  11073  cau3lem  11125  maxleb  11227  rexico  11232  negfi  11238  climshft  11314  zsumdc  11394  fsum3  11397  fsum00  11472  zproddc  11589  fprodseq  11593  dvdsval2  11799  moddvds  11808  negdvdsb  11816  dvdsnegb  11817  dvdscmulr  11829  dvdsmulcr  11830  dvdssub2  11844  fzo0dvdseq  11865  ltoddhalfle  11900  dvdsgcdb  12016  gcdzeq  12025  dvdssqlem  12033  lcmeq0  12073  lcmdvdsb  12086  coprmgcdb  12090  ncoprmgcdne1b  12091  cncongr  12107  isprm2lem  12118  dvdsprime  12124  dvdsprm  12139  coprm  12146  euclemma  12148  rpexp  12155  prmdiveq  12238  hashgcdlem  12240  odzdvds  12247  pythagtrip  12285  pcdvdsb  12321  pc2dvds  12331  pcprmpw2  12334  pcprmpw  12335  enct  12436  intopsn  12791  isgrpid2  12918  isgrpinv  12931  ringinvnz1ne0  13231  ringinvnzdiv  13232  unitmulclb  13288  dvreq1  13316  lssats2  13505  lspsneq0  13517  toponcomb  13613  tgss3  13663  isopn3  13710  neiint  13730  neipsm  13739  opnneissb  13740  opnssneib  13741  tpnei  13745  opnneiid  13749  restopnb  13766  tgcn  13793  tgcnp  13794  iscnp4  13803  cnpnei  13804  cnntr  13810  lmss  13831  upxp  13857  txcn  13860  txlm  13864  hmeoopn  13896  hmeocld  13897  xblm  14002  blssexps  14014  blssex  14015  isxms2  14037  neibl  14076  metss  14079  metrest  14091  metcnp3  14096  ivthinclemlr  14200  ivthinclemur  14202  cnplimccntop  14224  eflt  14281  lgsdir2lem4  14517  lgsne0  14524  m1lgs  14537  bj-charfunbi  14648  subctctexmid  14835  triap  14862  iswomni0  14884