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	|- ( 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 128	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 49	1 |- ( ph -> ( ps <-> ch ) )

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  667  pm5.21  696  nbn2  698  2falsed  703  pm5.21ndd  706  oibabs  715  orbi2d  791  con4biddc  858  con1bidc  875  con1bdc  879  dedlema  971  dedlemb  972  xorbin  1395  albi  1479  19.21ht  1592  exbi  1615  19.23t  1688  equequ1  1723  equequ2  1724  equsexd  1740  dral1  1741  cbv2h  1759  cbv2w  1761  sbequ12  1782  sbiedh  1798  drex1  1809  ax11b  1837  sbequ  1851  sbft  1859  sb56  1897  cbvexdh  1938  eupickb  2123  eupickbi  2124  elequ1  2168  elequ2  2169  ceqsalt  2786  ceqex  2887  mob2  2940  euxfr2dc  2945  reu6  2949  sbciegft  3016  csbiebt  3120  sseq1  3202  reupick  3443  reupick2  3445  disjeq2  4010  disjeq1  4013  exmidsssnc  4232  copsexg  4273  euotd  4283  poeq2  4331  sotritric  4355  sotritrieq  4356  seeq1  4370  seeq2  4371  alxfr  4492  ralxfrd  4493  rexxfrd  4494  ordelsuc  4537  sosng  4732  iss  4988  iotaval  5226  funeq  5274  funssres  5296  f0dom0  5447  tz6.12c  5584  fnbrfvb  5597  ssimaex  5618  fvimacnv  5673  elpreima  5677  fsn  5730  fconst2g  5773  elunirn  5809  f1ocnvfvb  5823  foeqcnvco  5833  f1eqcocnv  5834  fliftfun  5839  isose  5864  isopo  5866  isoso  5868  f1oiso2  5870  eusvobj2  5904  oprabid  5950  f1opw2  6124  op1steq  6232  rntpos  6310  frecabcl  6452  nnsucelsuc  6544  nnsucsssuc  6545  nnsseleq  6554  nnaord  6562  nnmord  6570  nnaordex  6581  nnawordex  6582  nnm00  6583  erexb  6612  swoord1  6616  swoord2  6617  iinerm  6661  fundmen  6860  mapxpen  6904  ssenen  6907  nneneq  6913  nndomo  6920  fidifsnen  6926  en1eqsnbi  7008  suplub2ti  7060  isoti  7066  ordiso2  7094  ordiso  7095  ctm  7168  ctssdc  7172  enomni  7198  enmkv  7221  enwomni  7229  pm54.43  7250  pr2ne  7252  ltexnqq  7468  genprndl  7581  genprndu  7582  nqprl  7611  nqpru  7612  1idprl  7650  1idpru  7651  ltexprlemrnd  7665  ltaprg  7679  recexprlemrnd  7689  cauappcvgprlemrnd  7710  caucvgprlemrnd  7733  caucvgprprlemrnd  7761  suplocexprlemrl  7777  suplocexprlemru  7779  map2psrprg  7865  ltxrlt  8085  lttri3  8099  addlsub  8389  addid0  8392  ltadd2  8438  eqord1  8502  reapti  8598  apreap  8606  ltmul1  8611  apreim  8622  ltleap  8651  mulap0b  8674  recapb  8690  apmul1  8807  rerecapb  8862  lt2msq  8905  nnsub  9021  zltnle  9363  zleloe  9364  zrevaddcl  9367  zltp1le  9371  zapne  9391  nn0n0n1ge2b  9396  zdiv  9405  nneo  9420  zeo2  9423  qrevaddcl  9709  npnflt  9881  nmnfgt  9884  xltneg  9902  xleadd1  9941  iccid  9991  zltaddlt1le  10073  fzn  10108  0fz1  10111  uzsplit  10158  fzm1  10166  fzrevral  10171  ssfzo12bi  10292  qltnle  10313  ioo0  10328  ioom  10329  ico0  10330  ioc0  10331  flqge  10351  modqid2  10422  modqmuladd  10437  frec2uzlt2d  10475  seqf1oglem1  10590  qsqeqor  10721  nn0ltexp2  10780  len0nnbi  10948  shftlem  10960  shftuz  10961  caucvgrelemcau  11124  sqrtsq  11188  abs00ap  11206  cau3lem  11258  maxleb  11360  rexico  11365  negfi  11371  climshft  11447  zsumdc  11527  fsum3  11530  fsum00  11605  zproddc  11722  fprodseq  11726  dvdsval2  11933  moddvds  11942  negdvdsb  11950  dvdsnegb  11951  dvdscmulr  11963  dvdsmulcr  11964  dvdssub2  11978  fzo0dvdseq  11999  ltoddhalfle  12034  dvdsgcdb  12150  gcdzeq  12159  dvdssqlem  12167  lcmeq0  12209  lcmdvdsb  12222  coprmgcdb  12226  ncoprmgcdne1b  12227  cncongr  12243  isprm2lem  12254  dvdsprime  12260  dvdsprm  12275  coprm  12282  euclemma  12284  rpexp  12291  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  pythagtrip  12421  pcdvdsb  12458  pc2dvds  12468  pcprmpw2  12471  pcprmpw  12472  enct  12590  intopsn  12950  gsumfzval  12974  isgrpid2  13112  isgrpinv  13126  f1ghm0to0  13342  ringinvnz1ne0  13545  ringinvnzdiv  13546  unitmulclb  13610  dvreq1  13638  isnzr2  13680  rrgeq0  13761  domneq0  13768  lssats2  13910  lspsneq0  13922  znunit  14147  toponcomb  14196  tgss3  14246  isopn3  14293  neiint  14313  neipsm  14322  opnneissb  14323  opnssneib  14324  tpnei  14328  opnneiid  14332  restopnb  14349  tgcn  14376  tgcnp  14377  iscnp4  14386  cnpnei  14387  cnntr  14393  lmss  14414  upxp  14440  txcn  14443  txlm  14447  hmeoopn  14479  hmeocld  14480  xblm  14585  blssexps  14597  blssex  14598  isxms2  14620  neibl  14659  metss  14662  metrest  14674  metcnp3  14679  ivthinclemlr  14791  ivthinclemur  14793  cnplimccntop  14824  eflt  14910  lgsdir2lem4  15147  lgsne0  15154  gausslemma2dlem1a  15174  lgsquadlem1  15191  m1lgs  15192  bj-charfunbi  15303  subctctexmid  15491  triap  15519  iswomni0  15541