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  1188  3adant1l  1257  reu6  2996  sbc2iegf  3103  sbcralt  3109  sbcrext  3110  indifdir  3465  pofun  4415  poinxp  4801  ssimaex  5716  fndmdif  5761  dffo4  5803  fcompt  5825  fconst2g  5877  foco2  5904  foeqcnvco  5941  f1eqcocnv  5942  fliftel1  5945  isores3  5966  acexmid  6027  suppssdc  6438  tfrlemi14d  6542  tfrcl  6573  dom2lem  6988  fiintim  7166  ordiso2  7294  mkvprop  7417  lt2addnq  7684  lt2mulnq  7685  ltexnqq  7688  genpdf  7788  addnqprl  7809  addnqpru  7810  addlocpr  7816  recexprlemopl  7905  caucvgsrlemgt1  8075  add4  8399  cnegex  8416  ltleadd  8685  zextle  9632  peano5uzti  9649  fnn0ind  9657  xrlttr  10091  xaddass  10165  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  fzaddel  10356  fzrev  10381  exbtwnzlemshrink  10571  xqltnle  10590  seq3val  10785  iseqf1olemab  10827  seqf1og  10846  exp3vallem  10865  mulexp  10903  expadd  10906  expmul  10909  leexp1a  10919  bccl  11092  hashfacen  11163  wrdnval  11210  swrdccat3blem  11386  ovshftex  11459  2shfti  11471  caucvgre  11621  cvg1nlemcau  11624  resqrexlemcvg  11659  cau3lem  11754  rexico  11861  iooinsup  11917  climmpt  11940  subcn2  11951  climrecvg1n  11988  climcvg1nlem  11989  climcaucn  11991  mertenslem2  12177  eftlcl  12329  reeftlcl  12330  dvdsext  12496  3dvds  12505  sqoddm1div8z  12527  bezoutlemaz  12654  bezoutr1  12684  dvdslcm  12721  lcmeq0  12723  lcmcl  12724  lcmneg  12726  lcmdvds  12731  coprmgcdb  12740  dvdsprime  12774  pc2dvds  12983  prmpwdvds  13008  infpnlem1  13012  1arith  13020  resmhm  13650  resmhm2b  13652  mhmco  13653  mhmima  13654  gsumwsubmcl  13659  dfgrp2  13690  mulgfng  13791  subgintm  13865  ghmmhmb  13921  resghm  13927  islmod  14387  islmodd  14389  cnco  15032  cnss1  15037  tx2cn  15081  upxp  15083  metss  15305  txmetcnp  15329  cncfss  15394  plyaddlem1  15558  plymullem1  15559  cosz12  15591  gausslemma2dlem4  15883  egrsubgr  16204  bj-findis  16695