Theorem 3adant2 1047

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
3adant2	|- ( ( ph /\ th /\ ps ) -> ch )

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 1026	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ th /\ ps ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3686  suc11g  4704  soinxp  4845  funopg  5411  fnco  5491  dff1o2  5644  fnimapr  5763  fvun1  5769  fvmptt  5797  fnreseql  5819  fvpr1g  5921  fvpr2g  5922  f1elima  5979  f1ocnvfvb  5986  ovexg  6119  oprssov  6231  poxp  6468  smoiso  6573  rdgivallem  6652  nndi  6759  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnaword  6784  nnawordi  6788  ecopovtrn  6906  ecopovtrng  6909  mapsnd  6970  xpdom3m  7132  mapxpen  7148  findcard  7192  fisseneq  7242  resfnfinfinss  7253  funrnfi  7256  netap  7620  2omotaplemap  7623  ltsopi  7687  addcanpig  7701  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltmnqg  7768  prarloclemarch2  7786  nnanq0  7825  distrnq0  7826  distnq0r  7830  prltlu  7854  prarloclem5  7867  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  axpre-mulext  8255  adddir  8317  axltwlin  8393  axlttrn  8394  ltleletr  8407  letr  8408  nnncan1  8563  npncan3  8565  pnpcan2  8567  subdi  8713  subdir  8714  reapcotr  8928  divmulap  9007  div23ap  9023  div13ap  9025  muldivdirap  9039  divsubdirap  9040  divcanap7  9053  ltmul2  9188  lemul2  9189  lemul2a  9191  lediv1  9201  ltmuldiv2  9207  lemuldiv2  9214  squeeze0  9236  nndivtr  9348  bndndx  9566  nn0n0n1ge2  9719  fnn0ind  9766  addlelt  10179  xrletr  10220  xrltne  10225  xleadd2a  10286  xleadd1  10287  xltadd2  10289  iooneg  10400  iccneg  10401  icoshft  10402  icoshftf1o  10403  zltaddlt1le  10420  fztri3or  10453  fzdcel  10454  fzen  10457  uzsubsubfz  10462  fzrevral2  10523  fzshftral  10525  fz0fzdiffz0  10547  elfzmlbp  10549  elfzo  10566  nelfzo  10569  fzoaddel2  10618  fzosubel2  10623  elfzom1p1elfzo  10642  ssfzo12bi  10653  subfzo0  10671  flltdivnn0lt  10752  modqmulnn  10792  modfzo0difsn  10845  expdivap  11040  expubnd  11046  mulbinom2  11106  bernneq2  11112  ccatval1  11379  ccatval3  11381  ccatfv0  11385  ccatval1lsw  11386  ccatws1lenp1bg  11417  pfxsuffeqwrdeq  11484  pfxsuff1eqwrdeq  11485  swrdswrd  11491  pfxpfx  11494  wrd2ind  11509  swrdccatin1  11511  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem3  11518  swrdccat  11521  pfxccatpfx1  11522  pfxccatpfx2  11523  swrdccat3blem  11525  shftuz  11596  shftval2  11605  abs3dif  11886  xrmaxlesup  12041  xrltmininf  12052  xrlemininf  12053  sin02gt0  12547  dvdsval2  12573  dvdscmul  12601  dvdsmulc  12602  ndvdssub  12713  rpmulgcd  12819  cncongr1  12897  cncongr2  12898  isprm3  12912  coprimeprodsq  13056  pythagtriplem12  13074  pythagtriplem14  13076  pcmul  13100  pcdiv  13101  pcqcl  13105  pcqdiv  13106  pcdvdsb  13119  ercpbl  13701  mgmb1mgm1  13737  grpinvid1  13906  grpinvid2  13907  grpasscan1  13917  grpasscan2  13918  grpinvadd  13932  grpsubf  13933  grpsubrcan  13935  grpinvsub  13936  grpsubeq0  13940  grpsubadd0sub  13941  grppncan  13945  grpnpcan  13946  mulgnn0p1  13985  mulgaddcomlem  13997  mulginvcom  13999  mulginvinv  14000  subgsubcl  14037  subgsub  14038  eqglact  14077  quselbasg  14082  quseccl0g  14083  qussub  14089  ghmsub  14103  subcmnd  14186  rng1zrlem  14307  dvrcl  14491  unitdvcl  14492  dvrcan1  14496  dvrcan3  14497  dvreq1  14498  subrgdv  14595  lmodvsubval2  14728  lmodprop2d  14734  zndvds  15033  ascldimul  15080  ntrin  15274  elnei  15302  cnrest2  15386  psmetsym  15479  psmetge0  15481  xmetge0  15515  xmetsym  15518  cnmet  15680  rpcxpsub  16063  rpdivcxp  16066  logbleb  16116  logblt  16117  lgsmodeq  16262  lgsmulsqcoprm  16263  gausslemma2dlem1a  16275  2lgsoddprmlem2  16323  upgrpredgv  16485  issubgr2  16597  uhgrissubgr  16600  egrsubgr  16602  upgrwlkvtxedg  16703  clwwlk1loop  16738  clwwlkccatlem  16739  clwwlknonex2lem2  16777  bj-peano4  17079