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  447  impbida  591  notbi  661  pm5.21  690  nbn2  692  2falsed  697  pm5.21ndd  700  oibabs  709  orbi2d  785  con4biddc  852  con1bidc  869  con1bdc  873  dedlema  964  dedlemb  965  xorbin  1379  albi  1461  19.21ht  1574  exbi  1597  19.23t  1670  equequ1  1705  equequ2  1706  equsexd  1722  dral1  1723  cbv2h  1741  cbv2w  1743  sbequ12  1764  sbiedh  1780  drex1  1791  ax11b  1819  sbequ  1833  sbft  1841  sb56  1878  cbvexdh  1919  eupickb  2100  eupickbi  2101  elequ1  2145  elequ2  2146  ceqsalt  2756  ceqex  2857  mob2  2910  euxfr2dc  2915  reu6  2919  sbciegft  2985  csbiebt  3088  sseq1  3170  reupick  3411  reupick2  3413  disjeq2  3968  disjeq1  3971  exmidsssnc  4187  copsexg  4227  euotd  4237  poeq2  4283  sotritric  4307  sotritrieq  4308  seeq1  4322  seeq2  4323  alxfr  4444  ralxfrd  4445  rexxfrd  4446  ordelsuc  4487  sosng  4682  iss  4935  iotaval  5169  funeq  5216  funssres  5238  f0dom0  5389  tz6.12c  5524  fnbrfvb  5535  ssimaex  5555  fvimacnv  5609  elpreima  5613  fsn  5666  fconst2g  5709  elunirn  5743  f1ocnvfvb  5757  foeqcnvco  5767  f1eqcocnv  5768  fliftfun  5773  isose  5798  isopo  5800  isoso  5802  f1oiso2  5804  eusvobj2  5837  oprabid  5883  f1opw2  6053  op1steq  6156  rntpos  6234  frecabcl  6376  nnsucelsuc  6468  nnsucsssuc  6469  nnsseleq  6478  nnaord  6486  nnmord  6494  nnaordex  6505  nnawordex  6506  nnm00  6507  erexb  6536  swoord1  6540  swoord2  6541  iinerm  6583  fundmen  6782  mapxpen  6824  ssenen  6827  nneneq  6833  nndomo  6840  fidifsnen  6846  en1eqsnbi  6924  suplub2ti  6976  isoti  6982  ordiso2  7010  ordiso  7011  ctm  7084  ctssdc  7088  enomni  7113  enmkv  7136  enwomni  7144  pm54.43  7160  pr2ne  7162  ltexnqq  7363  genprndl  7476  genprndu  7477  nqprl  7506  nqpru  7507  1idprl  7545  1idpru  7546  ltexprlemrnd  7560  ltaprg  7574  recexprlemrnd  7584  cauappcvgprlemrnd  7605  caucvgprlemrnd  7628  caucvgprprlemrnd  7656  suplocexprlemrl  7672  suplocexprlemru  7674  map2psrprg  7760  ltxrlt  7978  lttri3  7992  addlsub  8282  addid0  8285  ltadd2  8331  eqord1  8395  reapti  8491  apreap  8499  ltmul1  8504  apreim  8515  ltleap  8544  mulap0b  8566  apmul1  8698  lt2msq  8795  nnsub  8910  zltnle  9251  zleloe  9252  zrevaddcl  9255  zltp1le  9259  zapne  9279  nn0n0n1ge2b  9284  zdiv  9293  nneo  9308  zeo2  9311  qrevaddcl  9596  npnflt  9765  nmnfgt  9768  xltneg  9786  xleadd1  9825  iccid  9875  zltaddlt1le  9957  fzn  9991  0fz1  9994  uzsplit  10041  fzm1  10049  fzrevral  10054  ssfzo12bi  10174  qltnle  10195  ioo0  10209  ioom  10210  ico0  10211  ioc0  10212  flqge  10231  modqid2  10300  modqmuladd  10315  frec2uzlt2d  10353  qsqeqor  10579  nn0ltexp2  10637  shftlem  10773  shftuz  10774  caucvgrelemcau  10937  sqrtsq  11001  abs00ap  11019  cau3lem  11071  maxleb  11173  rexico  11178  negfi  11184  climshft  11260  zsumdc  11340  fsum3  11343  fsum00  11418  zproddc  11535  fprodseq  11539  dvdsval2  11745  moddvds  11754  negdvdsb  11762  dvdsnegb  11763  dvdscmulr  11775  dvdsmulcr  11776  dvdssub2  11790  fzo0dvdseq  11810  ltoddhalfle  11845  dvdsgcdb  11961  gcdzeq  11970  dvdssqlem  11978  lcmeq0  12018  lcmdvdsb  12031  coprmgcdb  12035  ncoprmgcdne1b  12036  cncongr  12052  isprm2lem  12063  dvdsprime  12069  dvdsprm  12084  coprm  12091  euclemma  12093  rpexp  12100  prmdiveq  12183  hashgcdlem  12185  odzdvds  12192  pythagtrip  12230  pcdvdsb  12266  pc2dvds  12276  pcprmpw2  12279  pcprmpw  12280  enct  12381  intopsn  12614  isgrpid2  12736  toponcomb  12785  tgss3  12837  isopn3  12884  neiint  12904  neipsm  12913  opnneissb  12914  opnssneib  12915  tpnei  12919  opnneiid  12923  restopnb  12940  tgcn  12967  tgcnp  12968  iscnp4  12977  cnpnei  12978  cnntr  12984  lmss  13005  upxp  13031  txcn  13034  txlm  13038  hmeoopn  13070  hmeocld  13071  xblm  13176  blssexps  13188  blssex  13189  isxms2  13211  neibl  13250  metss  13253  metrest  13265  metcnp3  13270  ivthinclemlr  13374  ivthinclemur  13376  cnplimccntop  13398  eflt  13455  lgsdir2lem4  13691  lgsne0  13698  bj-charfunbi  13811  subctctexmid  13999  triap  14026  iswomni0  14048