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  6578  rdgivallem  6657  nndi  6764  nndir  6768  fnsnsplitdc  6783  nnaord  6787  nnaordr  6788  nnaword  6789  nnawordi  6793  ecopovtrn  6911  ecopovtrng  6914  mapsnd  6976  xpdom3m  7138  mapxpen  7154  findcard  7198  fisseneq  7248  resfnfinfinss  7259  funrnfi  7262  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  9724  fnn0ind  9772  addlelt  10185  xrletr  10226  xrltne  10231  xleadd2a  10292  xleadd1  10293  xltadd2  10295  iooneg  10406  iccneg  10407  icoshft  10408  icoshftf1o  10409  zltaddlt1le  10426  fztri3or  10459  fzdcel  10460  fzen  10463  uzsubsubfz  10468  fzrevral2  10529  fzshftral  10531  fz0fzdiffz0  10553  elfzmlbp  10555  elfzo  10572  nelfzo  10575  fzoaddel2  10624  fzosubel2  10629  elfzom1p1elfzo  10648  ssfzo12bi  10659  subfzo0  10677  flltdivnn0lt  10759  modqmulnn  10799  modfzo0difsn  10852  expdivap  11047  expubnd  11053  mulbinom2  11113  bernneq2  11119  ccatval1  11386  ccatval3  11388  ccatfv0  11392  ccatval1lsw  11393  ccatws1lenp1bg  11424  pfxsuffeqwrdeq  11491  pfxsuff1eqwrdeq  11492  swrdswrd  11498  pfxpfx  11501  wrd2ind  11516  swrdccatin1  11518  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem3  11525  swrdccat  11528  pfxccatpfx1  11529  pfxccatpfx2  11530  swrdccat3blem  11532  shftuz  11603  shftval2  11612  abs3dif  11893  xrmaxlesup  12049  xrltmininf  12060  xrlemininf  12061  sin02gt0  12555  dvdsval2  12581  dvdscmul  12609  dvdsmulc  12610  ndvdssub  12721  rpmulgcd  12827  cncongr1  12905  cncongr2  12906  isprm3  12920  coprimeprodsq  13064  pythagtriplem12  13082  pythagtriplem14  13084  pcmul  13108  pcdiv  13109  pcqcl  13113  pcqdiv  13114  pcdvdsb  13127  ercpbl  13710  mgmb1mgm1  13746  grpinvid1  13915  grpinvid2  13916  grpasscan1  13926  grpasscan2  13927  grpinvadd  13941  grpsubf  13942  grpsubrcan  13944  grpinvsub  13945  grpsubeq0  13949  grpsubadd0sub  13950  grppncan  13954  grpnpcan  13955  mulgnn0p1  13994  mulgaddcomlem  14006  mulginvcom  14008  mulginvinv  14009  subgsubcl  14046  subgsub  14047  eqglact  14086  quselbasg  14091  quseccl0g  14092  qussub  14098  ghmsub  14112  subcmnd  14226  rng1zrlem  14364  dvrcl  14550  unitdvcl  14551  dvrcan1  14555  dvrcan3  14556  dvreq1  14557  subrgdv  14654  lmodvsubval2  14787  lmodprop2d  14793  zndvds  15092  ascldimul  15139  ntrin  15367  elnei  15395  cnrest2  15479  psmetsym  15572  psmetge0  15574  xmetge0  15608  xmetsym  15611  cnmet  15773  rpcxpsub  16158  rpdivcxp  16161  logbleb  16214  logblt  16215  lgsmodeq  16386  lgsmulsqcoprm  16387  gausslemma2dlem1a  16399  2lgsoddprmlem2  16447  upgrpredgv  16609  issubgr2  16721  uhgrissubgr  16724  egrsubgr  16726  upgrwlkvtxedg  16827  clwwlk1loop  16862  clwwlkccatlem  16863  clwwlknonex2lem2  16901  bj-peano4  17203