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  4360  poinxp  4745  ssimaex  5642  fndmdif  5687  dffo4  5730  fcompt  5752  fconst2g  5801  foco2  5824  foeqcnvco  5861  f1eqcocnv  5862  fliftel1  5865  isores3  5886  acexmid  5945  tfrlemi14d  6421  tfrcl  6452  dom2lem  6865  fiintim  7030  ordiso2  7139  mkvprop  7262  lt2addnq  7519  lt2mulnq  7520  ltexnqq  7523  genpdf  7623  addnqprl  7644  addnqpru  7645  addlocpr  7651  recexprlemopl  7740  caucvgsrlemgt1  7910  add4  8235  cnegex  8252  ltleadd  8521  zextle  9466  peano5uzti  9483  fnn0ind  9491  xrlttr  9919  xaddass  9993  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  fzaddel  10183  fzrev  10208  exbtwnzlemshrink  10393  xqltnle  10412  seq3val  10607  iseqf1olemab  10649  seqf1og  10668  exp3vallem  10687  mulexp  10725  expadd  10728  expmul  10731  leexp1a  10741  bccl  10914  hashfacen  10983  wrdnval  11026  ovshftex  11163  2shfti  11175  caucvgre  11325  cvg1nlemcau  11328  resqrexlemcvg  11363  cau3lem  11458  rexico  11565  iooinsup  11621  climmpt  11644  subcn2  11655  climrecvg1n  11692  climcvg1nlem  11693  climcaucn  11695  mertenslem2  11880  eftlcl  12032  reeftlcl  12033  dvdsext  12199  3dvds  12208  sqoddm1div8z  12230  bezoutlemaz  12357  bezoutr1  12387  dvdslcm  12424  lcmeq0  12426  lcmcl  12427  lcmneg  12429  lcmdvds  12434  coprmgcdb  12443  dvdsprime  12477  pc2dvds  12686  prmpwdvds  12711  infpnlem1  12715  1arith  12723  resmhm  13352  resmhm2b  13354  mhmco  13355  mhmima  13356  gsumwsubmcl  13361  dfgrp2  13392  mulgfng  13493  subgintm  13567  ghmmhmb  13623  resghm  13629  islmod  14086  islmodd  14088  cnco  14726  cnss1  14731  tx2cn  14775  upxp  14777  metss  14999  txmetcnp  15023  cncfss  15088  plyaddlem1  15252  plymullem1  15253  cosz12  15285  gausslemma2dlem4  15574  bj-findis  15952