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  1164  3adant1l  1233  reu6  2969  sbc2iegf  3076  sbcralt  3082  sbcrext  3083  indifdir  3437  pofun  4377  poinxp  4762  ssimaex  5663  fndmdif  5708  dffo4  5751  fcompt  5773  fconst2g  5822  foco2  5845  foeqcnvco  5882  f1eqcocnv  5883  fliftel1  5886  isores3  5907  acexmid  5966  tfrlemi14d  6442  tfrcl  6473  dom2lem  6886  fiintim  7054  ordiso2  7163  mkvprop  7286  lt2addnq  7552  lt2mulnq  7553  ltexnqq  7556  genpdf  7656  addnqprl  7677  addnqpru  7678  addlocpr  7684  recexprlemopl  7773  caucvgsrlemgt1  7943  add4  8268  cnegex  8285  ltleadd  8554  zextle  9499  peano5uzti  9516  fnn0ind  9524  xrlttr  9952  xaddass  10026  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  fzaddel  10216  fzrev  10241  exbtwnzlemshrink  10428  xqltnle  10447  seq3val  10642  iseqf1olemab  10684  seqf1og  10703  exp3vallem  10722  mulexp  10760  expadd  10763  expmul  10766  leexp1a  10776  bccl  10949  hashfacen  11018  wrdnval  11061  swrdccat3blem  11230  ovshftex  11245  2shfti  11257  caucvgre  11407  cvg1nlemcau  11410  resqrexlemcvg  11445  cau3lem  11540  rexico  11647  iooinsup  11703  climmpt  11726  subcn2  11737  climrecvg1n  11774  climcvg1nlem  11775  climcaucn  11777  mertenslem2  11962  eftlcl  12114  reeftlcl  12115  dvdsext  12281  3dvds  12290  sqoddm1div8z  12312  bezoutlemaz  12439  bezoutr1  12469  dvdslcm  12506  lcmeq0  12508  lcmcl  12509  lcmneg  12511  lcmdvds  12516  coprmgcdb  12525  dvdsprime  12559  pc2dvds  12768  prmpwdvds  12793  infpnlem1  12797  1arith  12805  resmhm  13434  resmhm2b  13436  mhmco  13437  mhmima  13438  gsumwsubmcl  13443  dfgrp2  13474  mulgfng  13575  subgintm  13649  ghmmhmb  13705  resghm  13711  islmod  14168  islmodd  14170  cnco  14808  cnss1  14813  tx2cn  14857  upxp  14859  metss  15081  txmetcnp  15105  cncfss  15170  plyaddlem1  15334  plymullem1  15335  cosz12  15367  gausslemma2dlem4  15656  bj-findis  16114