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  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  1898  eupickb  2080  eupickbi  2081  ceqsalt  2712  ceqex  2812  mob2  2864  euxfr2dc  2869  reu6  2873  sbciegft  2939  csbiebt  3039  sseq1  3120  reupick  3360  reupick2  3362  disjeq2  3910  disjeq1  3913  exmidsssnc  4126  copsexg  4166  euotd  4176  poeq2  4222  sotritric  4246  sotritrieq  4247  seeq1  4261  seeq2  4262  alxfr  4382  ralxfrd  4383  rexxfrd  4384  ordelsuc  4421  sosng  4612  iss  4865  iotaval  5099  funeq  5143  funssres  5165  f0dom0  5316  tz6.12c  5451  fnbrfvb  5462  ssimaex  5482  fvimacnv  5535  elpreima  5539  fsn  5592  fconst2g  5635  elunirn  5667  f1ocnvfvb  5681  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  isose  5722  isopo  5724  isoso  5726  f1oiso2  5728  eusvobj2  5760  oprabid  5803  f1opw2  5976  op1steq  6077  rntpos  6154  frecabcl  6296  nnsucelsuc  6387  nnsucsssuc  6388  nnsseleq  6397  nnaord  6405  nnmord  6413  nnaordex  6423  nnawordex  6424  nnm00  6425  erexb  6454  swoord1  6458  swoord2  6459  iinerm  6501  fundmen  6700  mapxpen  6742  ssenen  6745  nneneq  6751  nndomo  6758  fidifsnen  6764  en1eqsnbi  6837  suplub2ti  6888  isoti  6894  ordiso2  6920  ordiso  6921  ctm  6994  ctssdc  6998  enomni  7011  pm54.43  7046  pr2ne  7048  ltexnqq  7216  genprndl  7329  genprndu  7330  nqprl  7359  nqpru  7360  1idprl  7398  1idpru  7399  ltexprlemrnd  7413  ltaprg  7427  recexprlemrnd  7437  cauappcvgprlemrnd  7458  caucvgprlemrnd  7481  caucvgprprlemrnd  7509  suplocexprlemrl  7525  suplocexprlemru  7527  map2psrprg  7613  ltxrlt  7830  lttri3  7844  addlsub  8132  addid0  8135  ltadd2  8181  eqord1  8245  reapti  8341  apreap  8349  ltmul1  8354  apreim  8365  ltleap  8394  mulap0b  8416  apmul1  8548  lt2msq  8644  nnsub  8759  zltnle  9100  zleloe  9101  zrevaddcl  9104  zltp1le  9108  zapne  9125  nn0n0n1ge2b  9130  zdiv  9139  nneo  9154  zeo2  9157  qrevaddcl  9436  npnflt  9598  nmnfgt  9601  xltneg  9619  xleadd1  9658  iccid  9708  zltaddlt1le  9789  fzn  9822  0fz1  9825  uzsplit  9872  fzm1  9880  fzrevral  9885  ssfzo12bi  10002  qltnle  10023  ioo0  10037  ioom  10038  ico0  10039  ioc0  10040  flqge  10055  modqid2  10124  modqmuladd  10139  frec2uzlt2d  10177  shftlem  10588  shftuz  10589  caucvgrelemcau  10752  sqrtsq  10816  abs00ap  10834  cau3lem  10886  maxleb  10988  rexico  10993  negfi  10999  climshft  11073  zsumdc  11153  fsum3  11156  fsum00  11231  dvdsval2  11496  moddvds  11502  negdvdsb  11509  dvdsnegb  11510  dvdscmulr  11522  dvdsmulcr  11523  dvdssub2  11535  fzo0dvdseq  11555  ltoddhalfle  11590  dvdsgcdb  11701  gcdzeq  11710  dvdssqlem  11718  lcmeq0  11752  lcmdvdsb  11765  coprmgcdb  11769  ncoprmgcdne1b  11770  cncongr  11786  isprm2lem  11797  dvdsprime  11803  dvdsprm  11817  coprm  11822  euclemma  11824  rpexp  11831  hashgcdlem  11903  enct  11946  toponcomb  12195  tgss3  12247  isopn3  12294  neiint  12314  neipsm  12323  opnneissb  12324  opnssneib  12325  tpnei  12329  opnneiid  12333  restopnb  12350  tgcn  12377  tgcnp  12378  iscnp4  12387  cnpnei  12388  cnntr  12394  lmss  12415  upxp  12441  txcn  12444  txlm  12448  hmeoopn  12480  hmeocld  12481  xblm  12586  blssexps  12598  blssex  12599  isxms2  12621  neibl  12660  metss  12663  metrest  12675  metcnp3  12680  ivthinclemlr  12784  ivthinclemur  12786  cnplimccntop  12808  subctctexmid  13196  triap  13224