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  4706  soinxp  4847  funopg  5414  fnco  5494  dff1o2  5647  fnimapr  5766  fvun1  5772  fvmptt  5800  fnreseql  5822  fvpr1g  5924  fvpr2g  5925  f1elima  5982  f1ocnvfvb  5989  ovexg  6122  oprssov  6234  poxp  6472  smoiso  6577  rdgivallem  6656  nndi  6763  nndir  6767  fnsnsplitdc  6782  nnaord  6786  nnaordr  6787  nnaword  6788  nnawordi  6792  ecopovtrn  6910  ecopovtrng  6913  mapsnd  6974  xpdom3m  7136  mapxpen  7152  findcard  7196  fisseneq  7246  resfnfinfinss  7257  funrnfi  7260  netap  7626  2omotaplemap  7629  ltsopi  7693  addcanpig  7707  addassnqg  7755  distrnqg  7760  ltsonq  7771  ltmnqg  7774  prarloclemarch2  7792  nnanq0  7831  distrnq0  7832  distnq0r  7836  prltlu  7860  prarloclem5  7873  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  ltpopr  7968  ltsopr  7969  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulextsr1lem  8153  mulextsr1  8154  axpre-mulext  8261  adddir  8323  axltwlin  8399  axlttrn  8400  ltleletr  8413  letr  8414  nnncan1  8569  npncan3  8571  pnpcan2  8573  subdi  8719  subdir  8720  reapcotr  8934  divmulap  9013  div23ap  9029  div13ap  9031  muldivdirap  9045  divsubdirap  9046  divcanap7  9059  ltmul2  9194  lemul2  9195  lemul2a  9197  lediv1  9207  ltmuldiv2  9213  lemuldiv2  9220  squeeze0  9242  nndivtr  9355  bndndx  9573  nn0n0n1ge2  9726  fnn0ind  9773  addlelt  10186  xrletr  10227  xrltne  10232  xleadd2a  10293  xleadd1  10294  xltadd2  10296  iooneg  10407  iccneg  10408  icoshft  10409  icoshftf1o  10410  zltaddlt1le  10427  fztri3or  10460  fzdcel  10461  fzen  10464  uzsubsubfz  10469  fzrevral2  10530  fzshftral  10532  fz0fzdiffz0  10554  elfzmlbp  10556  elfzo  10573  nelfzo  10576  fzoaddel2  10625  fzosubel2  10630  elfzom1p1elfzo  10649  ssfzo12bi  10660  subfzo0  10678  flltdivnn0lt  10760  modqmulnn  10800  modfzo0difsn  10853  expdivap  11048  expubnd  11054  mulbinom2  11114  bernneq2  11120  ccatval1  11387  ccatval3  11389  ccatfv0  11393  ccatval1lsw  11394  ccatws1lenp1bg  11425  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  swrdswrd  11499  pfxpfx  11502  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem3  11526  swrdccat  11529  pfxccatpfx1  11530  pfxccatpfx2  11531  swrdccat3blem  11533  shftuz  11604  shftval2  11613  abs3dif  11894  xrmaxlesup  12050  xrltmininf  12061  xrlemininf  12062  sin02gt0  12556  dvdsval2  12582  dvdscmul  12610  dvdsmulc  12611  ndvdssub  12722  rpmulgcd  12828  cncongr1  12906  cncongr2  12907  isprm3  12921  coprimeprodsq  13065  pythagtriplem12  13083  pythagtriplem14  13085  pcmul  13109  pcdiv  13110  pcqcl  13114  pcqdiv  13115  pcdvdsb  13128  ercpbl  13711  mgmb1mgm1  13747  grpinvid1  13916  grpinvid2  13917  grpasscan1  13927  grpasscan2  13928  grpinvadd  13942  grpsubf  13943  grpsubrcan  13945  grpinvsub  13946  grpsubeq0  13950  grpsubadd0sub  13951  grppncan  13955  grpnpcan  13956  mulgnn0p1  13995  mulgaddcomlem  14007  mulginvcom  14009  mulginvinv  14010  subgsubcl  14047  subgsub  14048  eqglact  14087  quselbasg  14092  quseccl0g  14093  qussub  14099  ghmsub  14113  subcmnd  14227  rng1zrlem  14365  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  dvreq1  14558  subrgdv  14655  lmodvsubval2  14788  lmodprop2d  14794  zndvds  15093  ascldimul  15140  ntrin  15350  elnei  15378  cnrest2  15462  psmetsym  15555  psmetge0  15557  xmetge0  15591  xmetsym  15594  cnmet  15756  rpcxpsub  16141  rpdivcxp  16144  logbleb  16197  logblt  16198  lgsmodeq  16369  lgsmulsqcoprm  16370  gausslemma2dlem1a  16382  2lgsoddprmlem2  16430  upgrpredgv  16592  issubgr2  16704  uhgrissubgr  16707  egrsubgr  16709  upgrwlkvtxedg  16810  clwwlk1loop  16845  clwwlkccatlem  16846  clwwlknonex2lem2  16884  bj-peano4  17186