Theorem adantll 476

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( th /\ ph ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 283	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

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 is referenced by:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1185  3adant1l  1254  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  indifdir  3460  pofun  4403  poinxp  4788  ssimaex  5695  fndmdif  5740  dffo4  5783  fcompt  5805  fconst2g  5854  foco2  5877  foeqcnvco  5914  f1eqcocnv  5915  fliftel1  5918  isores3  5939  acexmid  6000  tfrlemi14d  6479  tfrcl  6510  dom2lem  6923  fiintim  7093  ordiso2  7202  mkvprop  7325  lt2addnq  7591  lt2mulnq  7592  ltexnqq  7595  genpdf  7695  addnqprl  7716  addnqpru  7717  addlocpr  7723  recexprlemopl  7812  caucvgsrlemgt1  7982  add4  8307  cnegex  8324  ltleadd  8593  zextle  9538  peano5uzti  9555  fnn0ind  9563  xrlttr  9991  xaddass  10065  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  fzaddel  10255  fzrev  10280  exbtwnzlemshrink  10468  xqltnle  10487  seq3val  10682  iseqf1olemab  10724  seqf1og  10743  exp3vallem  10762  mulexp  10800  expadd  10803  expmul  10806  leexp1a  10816  bccl  10989  hashfacen  11058  wrdnval  11102  swrdccat3blem  11271  ovshftex  11330  2shfti  11342  caucvgre  11492  cvg1nlemcau  11495  resqrexlemcvg  11530  cau3lem  11625  rexico  11732  iooinsup  11788  climmpt  11811  subcn2  11822  climrecvg1n  11859  climcvg1nlem  11860  climcaucn  11862  mertenslem2  12047  eftlcl  12199  reeftlcl  12200  dvdsext  12366  3dvds  12375  sqoddm1div8z  12397  bezoutlemaz  12524  bezoutr1  12554  dvdslcm  12591  lcmeq0  12593  lcmcl  12594  lcmneg  12596  lcmdvds  12601  coprmgcdb  12610  dvdsprime  12644  pc2dvds  12853  prmpwdvds  12878  infpnlem1  12882  1arith  12890  resmhm  13520  resmhm2b  13522  mhmco  13523  mhmima  13524  gsumwsubmcl  13529  dfgrp2  13560  mulgfng  13661  subgintm  13735  ghmmhmb  13791  resghm  13797  islmod  14255  islmodd  14257  cnco  14895  cnss1  14900  tx2cn  14944  upxp  14946  metss  15168  txmetcnp  15192  cncfss  15257  plyaddlem1  15421  plymullem1  15422  cosz12  15454  gausslemma2dlem4  15743  bj-findis  16342