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  1163  3adant1l  1232  reu6  2950  sbc2iegf  3057  sbcralt  3063  sbcrext  3064  indifdir  3416  pofun  4344  poinxp  4729  ssimaex  5619  fndmdif  5664  dffo4  5707  fcompt  5729  fconst2g  5774  foco2  5797  foeqcnvco  5834  f1eqcocnv  5835  fliftel1  5838  isores3  5859  acexmid  5918  tfrlemi14d  6388  tfrcl  6419  dom2lem  6828  fiintim  6987  ordiso2  7096  mkvprop  7219  lt2addnq  7466  lt2mulnq  7467  ltexnqq  7470  genpdf  7570  addnqprl  7591  addnqpru  7592  addlocpr  7598  recexprlemopl  7687  caucvgsrlemgt1  7857  add4  8182  cnegex  8199  ltleadd  8467  zextle  9411  peano5uzti  9428  fnn0ind  9436  xrlttr  9864  xaddass  9938  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzaddel  10128  fzrev  10153  exbtwnzlemshrink  10320  xqltnle  10339  seq3val  10534  iseqf1olemab  10576  seqf1og  10595  exp3vallem  10614  mulexp  10652  expadd  10655  expmul  10658  leexp1a  10668  bccl  10841  hashfacen  10910  wrdnval  10947  ovshftex  10966  2shfti  10978  caucvgre  11128  cvg1nlemcau  11131  resqrexlemcvg  11166  cau3lem  11261  rexico  11368  iooinsup  11423  climmpt  11446  subcn2  11457  climrecvg1n  11494  climcvg1nlem  11495  climcaucn  11497  mertenslem2  11682  eftlcl  11834  reeftlcl  11835  dvdsext  12000  sqoddm1div8z  12030  bezoutlemaz  12143  bezoutr1  12173  dvdslcm  12210  lcmeq0  12212  lcmcl  12213  lcmneg  12215  lcmdvds  12220  coprmgcdb  12229  dvdsprime  12263  pc2dvds  12471  prmpwdvds  12496  infpnlem1  12500  1arith  12508  resmhm  13062  resmhm2b  13064  mhmco  13065  mhmima  13066  gsumwsubmcl  13071  dfgrp2  13102  mulgfng  13197  subgintm  13271  ghmmhmb  13327  resghm  13333  islmod  13790  islmodd  13792  cnco  14400  cnss1  14405  tx2cn  14449  upxp  14451  metss  14673  txmetcnp  14697  cncfss  14762  plyaddlem1  14926  plymullem1  14927  cosz12  14956  gausslemma2dlem4  15221  bj-findis  15541