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  1161  3adant1l  1230  reu6  2927  sbc2iegf  3034  sbcralt  3040  sbcrext  3041  indifdir  3392  pofun  4313  poinxp  4696  ssimaex  5578  fndmdif  5622  dffo4  5665  fcompt  5687  fconst2g  5732  foco2  5755  foeqcnvco  5791  f1eqcocnv  5792  fliftel1  5795  isores3  5816  acexmid  5874  tfrlemi14d  6334  tfrcl  6365  dom2lem  6772  fiintim  6928  ordiso2  7034  mkvprop  7156  lt2addnq  7403  lt2mulnq  7404  ltexnqq  7407  genpdf  7507  addnqprl  7528  addnqpru  7529  addlocpr  7535  recexprlemopl  7624  caucvgsrlemgt1  7794  add4  8118  cnegex  8135  ltleadd  8403  zextle  9344  peano5uzti  9361  fnn0ind  9369  xrlttr  9795  xaddass  9869  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzaddel  10059  fzrev  10084  exbtwnzlemshrink  10249  seq3val  10458  iseqf1olemab  10489  exp3vallem  10521  mulexp  10559  expadd  10562  expmul  10565  leexp1a  10575  bccl  10747  hashfacen  10816  ovshftex  10828  2shfti  10840  caucvgre  10990  cvg1nlemcau  10993  resqrexlemcvg  11028  cau3lem  11123  rexico  11230  iooinsup  11285  climmpt  11308  subcn2  11319  climrecvg1n  11356  climcvg1nlem  11357  climcaucn  11359  mertenslem2  11544  eftlcl  11696  reeftlcl  11697  dvdsext  11861  sqoddm1div8z  11891  bezoutlemaz  12004  bezoutr1  12034  dvdslcm  12069  lcmeq0  12071  lcmcl  12072  lcmneg  12074  lcmdvds  12079  coprmgcdb  12088  dvdsprime  12122  pc2dvds  12329  prmpwdvds  12353  infpnlem1  12357  1arith  12365  mhmco  12874  mhmima  12875  dfgrp2  12902  mulgfng  12987  subgintm  13058  islmod  13381  islmodd  13383  cnco  13724  cnss1  13729  tx2cn  13773  upxp  13775  metss  13997  txmetcnp  14021  cncfss  14073  cosz12  14204  bj-findis  14734