Theorem impbid 128

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 127	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 49	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  445  impbida  585  notbi  655  pm5.21  684  nbn2  686  2falsed  691  pm5.21ndd  694  oibabs  703  orbi2d  779  con4biddc  842  con1bidc  859  con1bdc  863  dedlema  953  dedlemb  954  xorbin  1362  albi  1444  19.21ht  1560  exbi  1583  19.23t  1655  equequ1  1688  equequ2  1689  elequ1  1690  elequ2  1691  equsexd  1707  dral1  1708  cbv2h  1724  sbequ12  1744  sbiedh  1760  drex1  1770  ax11b  1798  sbequ  1812  sbft  1820  sb56  1857  cbvexdh  1896  eupickb  2078  eupickbi  2079  ceqsalt  2707  ceqex  2807  mob2  2859  euxfr2dc  2864  reu6  2868  sbciegft  2934  csbiebt  3034  sseq1  3115  reupick  3355  reupick2  3357  disjeq2  3905  disjeq1  3908  exmidsssnc  4121  copsexg  4161  euotd  4171  poeq2  4217  sotritric  4241  sotritrieq  4242  seeq1  4256  seeq2  4257  alxfr  4377  ralxfrd  4378  rexxfrd  4379  ordelsuc  4416  sosng  4607  iss  4860  iotaval  5094  funeq  5138  funssres  5160  f0dom0  5311  tz6.12c  5444  fnbrfvb  5455  ssimaex  5475  fvimacnv  5528  elpreima  5532  fsn  5585  fconst2g  5628  elunirn  5660  f1ocnvfvb  5674  foeqcnvco  5684  f1eqcocnv  5685  fliftfun  5690  isose  5715  isopo  5717  isoso  5719  f1oiso2  5721  eusvobj2  5753  oprabid  5796  f1opw2  5969  op1steq  6070  rntpos  6147  frecabcl  6289  nnsucelsuc  6380  nnsucsssuc  6381  nnsseleq  6390  nnaord  6398  nnmord  6406  nnaordex  6416  nnawordex  6417  nnm00  6418  erexb  6447  swoord1  6451  swoord2  6452  iinerm  6494  fundmen  6693  mapxpen  6735  ssenen  6738  nneneq  6744  nndomo  6751  fidifsnen  6757  en1eqsnbi  6830  suplub2ti  6881  isoti  6887  ordiso2  6913  ordiso  6914  ctm  6987  ctssdc  6991  enomni  7004  pm54.43  7039  pr2ne  7041  ltexnqq  7209  genprndl  7322  genprndu  7323  nqprl  7352  nqpru  7353  1idprl  7391  1idpru  7392  ltexprlemrnd  7406  ltaprg  7420  recexprlemrnd  7430  cauappcvgprlemrnd  7451  caucvgprlemrnd  7474  caucvgprprlemrnd  7502  suplocexprlemrl  7518  suplocexprlemru  7520  map2psrprg  7606  ltxrlt  7823  lttri3  7837  addlsub  8125  addid0  8128  ltadd2  8174  eqord1  8238  reapti  8334  apreap  8342  ltmul1  8347  apreim  8358  ltleap  8387  mulap0b  8409  apmul1  8541  lt2msq  8637  nnsub  8752  zltnle  9093  zleloe  9094  zrevaddcl  9097  zltp1le  9101  zapne  9118  nn0n0n1ge2b  9123  zdiv  9132  nneo  9147  zeo2  9150  qrevaddcl  9429  npnflt  9591  nmnfgt  9594  xltneg  9612  xleadd1  9651  iccid  9701  zltaddlt1le  9782  fzn  9815  0fz1  9818  uzsplit  9865  fzm1  9873  fzrevral  9878  ssfzo12bi  9995  qltnle  10016  ioo0  10030  ioom  10031  ico0  10032  ioc0  10033  flqge  10048  modqid2  10117  modqmuladd  10132  frec2uzlt2d  10170  shftlem  10581  shftuz  10582  caucvgrelemcau  10745  sqrtsq  10809  abs00ap  10827  cau3lem  10879  maxleb  10981  rexico  10986  negfi  10992  climshft  11066  zsumdc  11146  fsum3  11149  fsum00  11224  dvdsval2  11485  moddvds  11491  negdvdsb  11498  dvdsnegb  11499  dvdscmulr  11511  dvdsmulcr  11512  dvdssub2  11524  fzo0dvdseq  11544  ltoddhalfle  11579  dvdsgcdb  11690  gcdzeq  11699  dvdssqlem  11707  lcmeq0  11741  lcmdvdsb  11754  coprmgcdb  11758  ncoprmgcdne1b  11759  cncongr  11775  isprm2lem  11786  dvdsprime  11792  dvdsprm  11806  coprm  11811  euclemma  11813  rpexp  11820  hashgcdlem  11892  enct  11935  toponcomb  12184  tgss3  12236  isopn3  12283  neiint  12303  neipsm  12312  opnneissb  12313  opnssneib  12314  tpnei  12318  opnneiid  12322  restopnb  12339  tgcn  12366  tgcnp  12367  iscnp4  12376  cnpnei  12377  cnntr  12383  lmss  12404  upxp  12430  txcn  12433  txlm  12437  hmeoopn  12469  hmeocld  12470  xblm  12575  blssexps  12587  blssex  12588  isxms2  12610  neibl  12649  metss  12652  metrest  12664  metcnp3  12669  ivthinclemlr  12773  ivthinclemur  12775  cnplimccntop  12797  subctctexmid  13185  triap  13213