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	|- ( ph -> ( ps -> ch ) )
impbid.2	|- ( ph -> ( ch -> ps ) )

Assertion

Ref	Expression
impbid	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		impbid.2	. . 3 |- ( ph -> ( ch -> ps ) )
3	1, 2	impbid21d 127	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 49	1 |- ( ph -> ( ps <-> ch ) )

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  446  impbida  586  notbi  656  pm5.21  685  nbn2  687  2falsed  692  pm5.21ndd  695  oibabs  704  orbi2d  780  con4biddc  843  con1bidc  860  con1bdc  864  dedlema  954  dedlemb  955  xorbin  1363  albi  1445  19.21ht  1561  exbi  1584  19.23t  1656  equequ1  1689  equequ2  1690  elequ1  1691  elequ2  1692  equsexd  1708  dral1  1709  cbv2h  1725  sbequ12  1745  sbiedh  1761  drex1  1771  ax11b  1799  sbequ  1813  sbft  1821  sb56  1858  cbvexdh  1899  eupickb  2081  eupickbi  2082  ceqsalt  2715  ceqex  2816  mob2  2868  euxfr2dc  2873  reu6  2877  sbciegft  2943  csbiebt  3044  sseq1  3125  reupick  3365  reupick2  3367  disjeq2  3918  disjeq1  3921  exmidsssnc  4134  copsexg  4174  euotd  4184  poeq2  4230  sotritric  4254  sotritrieq  4255  seeq1  4269  seeq2  4270  alxfr  4390  ralxfrd  4391  rexxfrd  4392  ordelsuc  4429  sosng  4620  iss  4873  iotaval  5107  funeq  5151  funssres  5173  f0dom0  5324  tz6.12c  5459  fnbrfvb  5470  ssimaex  5490  fvimacnv  5543  elpreima  5547  fsn  5600  fconst2g  5643  elunirn  5675  f1ocnvfvb  5689  foeqcnvco  5699  f1eqcocnv  5700  fliftfun  5705  isose  5730  isopo  5732  isoso  5734  f1oiso2  5736  eusvobj2  5768  oprabid  5811  f1opw2  5984  op1steq  6085  rntpos  6162  frecabcl  6304  nnsucelsuc  6395  nnsucsssuc  6396  nnsseleq  6405  nnaord  6413  nnmord  6421  nnaordex  6431  nnawordex  6432  nnm00  6433  erexb  6462  swoord1  6466  swoord2  6467  iinerm  6509  fundmen  6708  mapxpen  6750  ssenen  6753  nneneq  6759  nndomo  6766  fidifsnen  6772  en1eqsnbi  6845  suplub2ti  6896  isoti  6902  ordiso2  6928  ordiso  6929  ctm  7002  ctssdc  7006  enomni  7019  enmkv  7044  enwomni  7051  pm54.43  7063  pr2ne  7065  ltexnqq  7240  genprndl  7353  genprndu  7354  nqprl  7383  nqpru  7384  1idprl  7422  1idpru  7423  ltexprlemrnd  7437  ltaprg  7451  recexprlemrnd  7461  cauappcvgprlemrnd  7482  caucvgprlemrnd  7505  caucvgprprlemrnd  7533  suplocexprlemrl  7549  suplocexprlemru  7551  map2psrprg  7637  ltxrlt  7854  lttri3  7868  addlsub  8156  addid0  8159  ltadd2  8205  eqord1  8269  reapti  8365  apreap  8373  ltmul1  8378  apreim  8389  ltleap  8418  mulap0b  8440  apmul1  8572  lt2msq  8668  nnsub  8783  zltnle  9124  zleloe  9125  zrevaddcl  9128  zltp1le  9132  zapne  9149  nn0n0n1ge2b  9154  zdiv  9163  nneo  9178  zeo2  9181  qrevaddcl  9463  npnflt  9628  nmnfgt  9631  xltneg  9649  xleadd1  9688  iccid  9738  zltaddlt1le  9820  fzn  9853  0fz1  9856  uzsplit  9903  fzm1  9911  fzrevral  9916  ssfzo12bi  10033  qltnle  10054  ioo0  10068  ioom  10069  ico0  10070  ioc0  10071  flqge  10086  modqid2  10155  modqmuladd  10170  frec2uzlt2d  10208  shftlem  10620  shftuz  10621  caucvgrelemcau  10784  sqrtsq  10848  abs00ap  10866  cau3lem  10918  maxleb  11020  rexico  11025  negfi  11031  climshft  11105  zsumdc  11185  fsum3  11188  fsum00  11263  zproddc  11380  fprodseq  11384  dvdsval2  11532  moddvds  11538  negdvdsb  11545  dvdsnegb  11546  dvdscmulr  11558  dvdsmulcr  11559  dvdssub2  11571  fzo0dvdseq  11591  ltoddhalfle  11626  dvdsgcdb  11737  gcdzeq  11746  dvdssqlem  11754  lcmeq0  11788  lcmdvdsb  11801  coprmgcdb  11805  ncoprmgcdne1b  11806  cncongr  11822  isprm2lem  11833  dvdsprime  11839  dvdsprm  11853  coprm  11858  euclemma  11860  rpexp  11867  hashgcdlem  11939  enct  11982  toponcomb  12234  tgss3  12286  isopn3  12333  neiint  12353  neipsm  12362  opnneissb  12363  opnssneib  12364  tpnei  12368  opnneiid  12372  restopnb  12389  tgcn  12416  tgcnp  12417  iscnp4  12426  cnpnei  12427  cnntr  12433  lmss  12454  upxp  12480  txcn  12483  txlm  12487  hmeoopn  12519  hmeocld  12520  xblm  12625  blssexps  12637  blssex  12638  isxms2  12660  neibl  12699  metss  12702  metrest  12714  metcnp3  12719  ivthinclemlr  12823  ivthinclemur  12825  cnplimccntop  12847  eflt  12904  subctctexmid  13369  triap  13399