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  847  con1bidc  864  con1bdc  868  dedlema  959  dedlemb  960  xorbin  1374  albi  1456  19.21ht  1569  exbi  1592  19.23t  1665  equequ1  1700  equequ2  1701  equsexd  1717  dral1  1718  cbv2h  1736  cbv2w  1738  sbequ12  1759  sbiedh  1775  drex1  1786  ax11b  1814  sbequ  1828  sbft  1836  sb56  1873  cbvexdh  1914  eupickb  2095  eupickbi  2096  elequ1  2140  elequ2  2141  ceqsalt  2751  ceqex  2852  mob2  2905  euxfr2dc  2910  reu6  2914  sbciegft  2980  csbiebt  3083  sseq1  3164  reupick  3405  reupick2  3407  disjeq2  3962  disjeq1  3965  exmidsssnc  4181  copsexg  4221  euotd  4231  poeq2  4277  sotritric  4301  sotritrieq  4302  seeq1  4316  seeq2  4317  alxfr  4438  ralxfrd  4439  rexxfrd  4440  ordelsuc  4481  sosng  4676  iss  4929  iotaval  5163  funeq  5207  funssres  5229  f0dom0  5380  tz6.12c  5515  fnbrfvb  5526  ssimaex  5546  fvimacnv  5599  elpreima  5603  fsn  5656  fconst2g  5699  elunirn  5733  f1ocnvfvb  5747  foeqcnvco  5757  f1eqcocnv  5758  fliftfun  5763  isose  5788  isopo  5790  isoso  5792  f1oiso2  5794  eusvobj2  5827  oprabid  5870  f1opw2  6043  op1steq  6144  rntpos  6221  frecabcl  6363  nnsucelsuc  6455  nnsucsssuc  6456  nnsseleq  6465  nnaord  6473  nnmord  6481  nnaordex  6491  nnawordex  6492  nnm00  6493  erexb  6522  swoord1  6526  swoord2  6527  iinerm  6569  fundmen  6768  mapxpen  6810  ssenen  6813  nneneq  6819  nndomo  6826  fidifsnen  6832  en1eqsnbi  6910  suplub2ti  6962  isoti  6968  ordiso2  6996  ordiso  6997  ctm  7070  ctssdc  7074  enomni  7099  enmkv  7122  enwomni  7130  pm54.43  7142  pr2ne  7144  ltexnqq  7345  genprndl  7458  genprndu  7459  nqprl  7488  nqpru  7489  1idprl  7527  1idpru  7528  ltexprlemrnd  7542  ltaprg  7556  recexprlemrnd  7566  cauappcvgprlemrnd  7587  caucvgprlemrnd  7610  caucvgprprlemrnd  7638  suplocexprlemrl  7654  suplocexprlemru  7656  map2psrprg  7742  ltxrlt  7960  lttri3  7974  addlsub  8264  addid0  8267  ltadd2  8313  eqord1  8377  reapti  8473  apreap  8481  ltmul1  8486  apreim  8497  ltleap  8526  mulap0b  8548  apmul1  8680  lt2msq  8777  nnsub  8892  zltnle  9233  zleloe  9234  zrevaddcl  9237  zltp1le  9241  zapne  9261  nn0n0n1ge2b  9266  zdiv  9275  nneo  9290  zeo2  9293  qrevaddcl  9578  npnflt  9747  nmnfgt  9750  xltneg  9768  xleadd1  9807  iccid  9857  zltaddlt1le  9939  fzn  9973  0fz1  9976  uzsplit  10023  fzm1  10031  fzrevral  10036  ssfzo12bi  10156  qltnle  10177  ioo0  10191  ioom  10192  ico0  10193  ioc0  10194  flqge  10213  modqid2  10282  modqmuladd  10297  frec2uzlt2d  10335  qsqeqor  10561  nn0ltexp2  10619  shftlem  10754  shftuz  10755  caucvgrelemcau  10918  sqrtsq  10982  abs00ap  11000  cau3lem  11052  maxleb  11154  rexico  11159  negfi  11165  climshft  11241  zsumdc  11321  fsum3  11324  fsum00  11399  zproddc  11516  fprodseq  11520  dvdsval2  11726  moddvds  11735  negdvdsb  11743  dvdsnegb  11744  dvdscmulr  11756  dvdsmulcr  11757  dvdssub2  11771  fzo0dvdseq  11791  ltoddhalfle  11826  dvdsgcdb  11942  gcdzeq  11951  dvdssqlem  11959  lcmeq0  11999  lcmdvdsb  12012  coprmgcdb  12016  ncoprmgcdne1b  12017  cncongr  12033  isprm2lem  12044  dvdsprime  12050  dvdsprm  12065  coprm  12072  euclemma  12074  rpexp  12081  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  pythagtrip  12211  pcdvdsb  12247  pc2dvds  12257  pcprmpw2  12260  pcprmpw  12261  enct  12362  toponcomb  12626  tgss3  12678  isopn3  12725  neiint  12745  neipsm  12754  opnneissb  12755  opnssneib  12756  tpnei  12760  opnneiid  12764  restopnb  12781  tgcn  12808  tgcnp  12809  iscnp4  12818  cnpnei  12819  cnntr  12825  lmss  12846  upxp  12872  txcn  12875  txlm  12879  hmeoopn  12911  hmeocld  12912  xblm  13017  blssexps  13029  blssex  13030  isxms2  13052  neibl  13091  metss  13094  metrest  13106  metcnp3  13111  ivthinclemlr  13215  ivthinclemur  13217  cnplimccntop  13239  eflt  13296  lgsdir2lem4  13532  lgsne0  13539  bj-charfunbi  13653  subctctexmid  13841  triap  13868  iswomni0  13890