Theorem 3adant2 1018

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 997	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ th /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3ad2ant1  1020  3imp3i2an  1185  eupickb  2123  vtoclegft  2833  eqeu  2931  ifnebibdc  3601  suc11g  4590  soinxp  4730  funopg  5289  fnco  5363  dff1o2  5506  fnimapr  5618  fvun1  5624  fvmptt  5650  fnreseql  5669  fvpr1g  5765  fvpr2g  5766  f1elima  5817  f1ocnvfvb  5824  ovexg  5953  oprssov  6062  poxp  6287  smoiso  6357  rdgivallem  6436  nndi  6541  nndir  6545  fnsnsplitdc  6560  nnaord  6564  nnaordr  6565  nnaword  6566  nnawordi  6570  ecopovtrn  6688  ecopovtrng  6691  xpdom3m  6890  mapxpen  6906  findcard  6946  fisseneq  6990  resfnfinfinss  7000  funrnfi  7003  netap  7316  2omotaplemap  7319  ltsopi  7382  addcanpig  7396  addassnqg  7444  distrnqg  7449  ltsonq  7460  ltmnqg  7463  prarloclemarch2  7481  nnanq0  7520  distrnq0  7521  distnq0r  7525  prltlu  7549  prarloclem5  7562  distrlem1prl  7644  distrlem1pru  7645  distrlem5prl  7648  distrlem5pru  7649  ltpopr  7657  ltsopr  7658  ltexprlemm  7662  ltexprlemfl  7671  ltexprlemfu  7673  lttrsr  7824  ltsosr  7826  ltasrg  7832  recexgt0sr  7835  mulextsr1lem  7842  mulextsr1  7843  axpre-mulext  7950  adddir  8012  axltwlin  8089  axlttrn  8090  ltleletr  8103  letr  8104  nnncan1  8257  npncan3  8259  pnpcan2  8261  subdi  8406  subdir  8407  reapcotr  8619  divmulap  8696  div23ap  8712  div13ap  8714  muldivdirap  8728  divsubdirap  8729  divcanap7  8742  ltmul2  8877  lemul2  8878  lemul2a  8880  lediv1  8890  ltmuldiv2  8896  lemuldiv2  8903  squeeze0  8925  nndivtr  9026  bndndx  9242  nn0n0n1ge2  9390  fnn0ind  9436  addlelt  9837  xrletr  9877  xrltne  9882  xleadd2a  9943  xleadd1  9944  xltadd2  9946  iooneg  10057  iccneg  10058  icoshft  10059  icoshftf1o  10060  zltaddlt1le  10076  fztri3or  10108  fzdcel  10109  fzen  10112  uzsubsubfz  10116  fzrevral2  10175  fzshftral  10177  fz0fzdiffz0  10199  elfzmlbp  10201  elfzo  10218  nelfzo  10221  fzoaddel2  10263  fzosubel2  10265  elfzom1p1elfzo  10284  ssfzo12bi  10295  subfzo0  10312  flltdivnn0lt  10376  modqmulnn  10416  modfzo0difsn  10469  expdivap  10664  expubnd  10670  mulbinom2  10730  bernneq2  10735  shftuz  10964  shftval2  10973  abs3dif  11252  xrmaxlesup  11405  xrltmininf  11416  xrlemininf  11417  sin02gt0  11910  dvdsval2  11936  dvdscmul  11964  dvdsmulc  11965  ndvdssub  12074  rpmulgcd  12166  cncongr1  12244  cncongr2  12245  isprm3  12259  coprimeprodsq  12398  pythagtriplem12  12416  pythagtriplem14  12418  pcmul  12442  pcdiv  12443  pcqcl  12447  pcqdiv  12448  pcdvdsb  12461  ercpbl  12917  mgmb1mgm1  12954  grpinvid1  13127  grpinvid2  13128  grpasscan1  13138  grpasscan2  13139  grpinvadd  13153  grpsubf  13154  grpsubrcan  13156  grpinvsub  13157  grpsubeq0  13161  grpsubadd0sub  13162  grppncan  13166  grpnpcan  13167  mulgnn0p1  13206  mulgaddcomlem  13218  mulginvcom  13220  mulginvinv  13221  subgsubcl  13258  subgsub  13259  eqglact  13298  quselbasg  13303  quseccl0g  13304  qussub  13310  ghmsub  13324  subcmnd  13406  srg1zr  13486  dvrcl  13634  unitdvcl  13635  dvrcan1  13639  dvrcan3  13640  dvreq1  13641  subrgdv  13737  lmodvsubval2  13841  lmodprop2d  13847  zndvds  14148  ntrin  14303  elnei  14331  cnrest2  14415  psmetsym  14508  psmetge0  14510  xmetge0  14544  xmetsym  14547  cnmet  14709  rpcxpsub  15084  rpdivcxp  15087  logbleb  15134  logblt  15135  lgsmodeq  15202  lgsmulsqcoprm  15203  gausslemma2dlem1a  15215  2lgsoddprmlem2  15263  bj-peano4  15517