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  600  notbi  672  pm5.21  703  nbn2  705  2falsed  710  pm5.21ndd  713  oibabs  722  orbi2d  798  con4biddc  865  con1bidc  882  con1bdc  886  dedlema  978  dedlemb  979  xorbin  1429  albi  1517  19.21ht  1630  exbi  1653  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1778  dral1  1779  cbv2h  1797  cbv2w  1799  sbequ12  1820  sbiedh  1836  drex1  1847  ax11b  1875  sbequ  1889  sbft  1897  sb56  1935  cbvexdh  1976  eupickb  2162  eupickbi  2163  elequ1  2207  elequ2  2208  ceqsalt  2839  ceqex  2943  mob2  2996  euxfr2dc  3001  reu6  3005  sbciegft  3072  csbiebt  3177  sseq1  3260  reupick  3504  reupick2  3506  disjeq2  4088  disjeq1  4091  exmidsssnc  4315  copsexg  4359  euotd  4370  poeq2  4420  sotritric  4444  sotritrieq  4445  seeq1  4459  seeq2  4460  alxfr  4581  ralxfrd  4582  rexxfrd  4583  ordelsuc  4626  sosng  4822  iss  5083  iotaval  5323  funeq  5371  funssres  5394  f0dom0  5560  tz6.12c  5699  fnbrfvb  5714  ssimaex  5737  fvimacnv  5792  elpreima  5796  fsn  5848  fconst2g  5898  fndmexb  5906  elunirn  5938  f1ocnvfvb  5952  foeqcnvco  5962  f1eqcocnv  5963  fliftfun  5968  isose  5993  isopo  5995  isoso  5997  f1oiso2  5999  eusvobj2  6035  oprabid  6081  f1opw2  6260  op1steq  6372  fvn0elsuppb  6451  rntpos  6487  frecabcl  6629  nnsucelsuc  6723  nnsucsssuc  6724  nnsseleq  6733  nnaord  6741  nnmord  6749  nnaordex  6760  nnawordex  6761  nnm00  6762  erexb  6791  swoord1  6795  swoord2  6796  iinerm  6840  mapsnd  6922  fundmen  7046  dom1o  7068  mapxpen  7100  mapunen  7103  ssenen  7104  nneneq  7110  nndomo  7117  fidifsnen  7124  en1eqsnbi  7218  suplub2ti  7291  isoti  7297  ordiso2  7325  ordiso  7326  ctm  7399  ctssdc  7403  enomni  7429  enmkv  7452  enwomni  7460  pm54.43  7486  pr2ne  7488  ltexnqq  7719  genprndl  7832  genprndu  7833  nqprl  7862  nqpru  7863  1idprl  7901  1idpru  7902  ltexprlemrnd  7916  ltaprg  7930  recexprlemrnd  7940  cauappcvgprlemrnd  7961  caucvgprlemrnd  7984  caucvgprprlemrnd  8012  suplocexprlemrl  8028  suplocexprlemru  8030  map2psrprg  8116  ltxrlt  8335  lttri3  8349  addlsub  8639  addid0  8642  ltadd2  8689  eqord1  8753  reapti  8849  apreap  8857  ltmul1  8862  apreim  8873  ltleap  8902  mulap0b  8925  recapb  8941  apmul1  9058  rerecapb  9113  lt2msq  9156  nnsub  9272  zltnle  9619  zleloe  9620  zrevaddcl  9624  zltp1le  9628  zapne  9648  nn0n0n1ge2b  9653  zdiv  9662  nneo  9677  zeo2  9680  qrevaddcl  9972  npnflt  10144  nmnfgt  10147  xltneg  10165  xleadd1  10204  iccid  10254  zltaddlt1le  10337  fzn  10372  0fz1  10375  uzsplit  10422  fzm1  10430  fzrevral  10435  ssfzo12bi  10566  qltnle  10599  ioo0  10615  ioom  10616  ico0  10617  ioc0  10618  flqge  10638  modqid2  10709  modqmuladd  10724  frec2uzlt2d  10762  seqf1oglem1  10877  qsqeqor  11008  nn0ltexp2  11067  hashtpg  11212  len0nnbi  11252  ccats1pfxeqbi  11427  reuccatpfxs1  11432  shftlem  11494  shftuz  11495  caucvgrelemcau  11658  sqrtsq  11722  abs00ap  11740  cau3lem  11792  maxleb  11894  rexico  11899  negfi  11906  climshft  11982  zsumdc  12063  fsum3  12066  fsum00  12141  zproddc  12258  fprodseq  12262  dvdsval2  12469  moddvds  12478  negdvdsb  12486  dvdsnegb  12487  dvdscmulr  12499  dvdsmulcr  12500  dvdssub2  12514  fzo0dvdseq  12536  ltoddhalfle  12572  dvdsgcdb  12702  gcdzeq  12711  dvdssqlem  12719  lcmeq0  12761  lcmdvdsb  12774  coprmgcdb  12778  ncoprmgcdne1b  12779  cncongr  12795  isprm2lem  12806  dvdsprime  12812  dvdsprm  12827  coprm  12834  euclemma  12836  rpexp  12843  prmdiveq  12926  hashgcdlem  12928  odzdvds  12936  pythagtrip  12974  pcdvdsb  13011  pc2dvds  13021  pcprmpw2  13024  pcprmpw  13025  enct  13173  intopsn  13569  gsumfzval  13593  isgrpid2  13742  isgrpinv  13756  f1ghm0to0  13978  ringinvnz1ne0  14182  ringinvnzdiv  14183  unitmulclb  14248  dvreq1  14276  isnzr2  14318  rrgeq0  14399  domneq0  14407  lssats2  14549  lspsneq0  14561  znunit  14794  toponcomb  14880  tgss3  14930  isopn3  14977  neiint  14997  neipsm  15006  opnneissb  15007  opnssneib  15008  tpnei  15012  opnneiid  15016  restopnb  15033  tgcn  15060  tgcnp  15061  iscnp4  15070  cnpnei  15071  cnntr  15077  lmss  15098  upxp  15124  txcn  15127  txlm  15131  hmeoopn  15163  hmeocld  15164  xblm  15269  blssexps  15281  blssex  15282  isxms2  15304  neibl  15343  metss  15346  metrest  15358  metcnp3  15363  ivthinclemlr  15489  ivthinclemur  15491  cnplimccntop  15522  eflt  15627  dvdsppwf1o  15844  lgsdir2lem4  15891  lgsne0  15898  gausslemma2dlem1a  15918  lgsquadlem1  15937  m1lgs  15945  uhgr0vb  16066  ausgrusgrben  16150  ushgredgedg  16208  ushgredgedgloop  16210  usgr0vb  16215  loopclwwlkn1b  16401  eupth2lem3lem4fi  16455  bj-charfunbi  16568  subctctexmid  16761  triap  16800  iswomni0  16823