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  2962  sbc2iegf  3069  sbcralt  3075  sbcrext  3076  indifdir  3429  pofun  4359  poinxp  4744  ssimaex  5640  fndmdif  5685  dffo4  5728  fcompt  5750  fconst2g  5799  foco2  5822  foeqcnvco  5859  f1eqcocnv  5860  fliftel1  5863  isores3  5884  acexmid  5943  tfrlemi14d  6419  tfrcl  6450  dom2lem  6863  fiintim  7028  ordiso2  7137  mkvprop  7260  lt2addnq  7517  lt2mulnq  7518  ltexnqq  7521  genpdf  7621  addnqprl  7642  addnqpru  7643  addlocpr  7649  recexprlemopl  7738  caucvgsrlemgt1  7908  add4  8233  cnegex  8250  ltleadd  8519  zextle  9464  peano5uzti  9481  fnn0ind  9489  xrlttr  9917  xaddass  9991  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  fzaddel  10181  fzrev  10206  exbtwnzlemshrink  10391  xqltnle  10410  seq3val  10605  iseqf1olemab  10647  seqf1og  10666  exp3vallem  10685  mulexp  10723  expadd  10726  expmul  10729  leexp1a  10739  bccl  10912  hashfacen  10981  wrdnval  11024  ovshftex  11130  2shfti  11142  caucvgre  11292  cvg1nlemcau  11295  resqrexlemcvg  11330  cau3lem  11425  rexico  11532  iooinsup  11588  climmpt  11611  subcn2  11622  climrecvg1n  11659  climcvg1nlem  11660  climcaucn  11662  mertenslem2  11847  eftlcl  11999  reeftlcl  12000  dvdsext  12166  3dvds  12175  sqoddm1div8z  12197  bezoutlemaz  12324  bezoutr1  12354  dvdslcm  12391  lcmeq0  12393  lcmcl  12394  lcmneg  12396  lcmdvds  12401  coprmgcdb  12410  dvdsprime  12444  pc2dvds  12653  prmpwdvds  12678  infpnlem1  12682  1arith  12690  resmhm  13319  resmhm2b  13321  mhmco  13322  mhmima  13323  gsumwsubmcl  13328  dfgrp2  13359  mulgfng  13460  subgintm  13534  ghmmhmb  13590  resghm  13596  islmod  14053  islmodd  14055  cnco  14693  cnss1  14698  tx2cn  14742  upxp  14744  metss  14966  txmetcnp  14990  cncfss  15055  plyaddlem1  15219  plymullem1  15220  cosz12  15252  gausslemma2dlem4  15541  bj-findis  15915