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  2926  sbc2iegf  3033  sbcralt  3039  sbcrext  3040  indifdir  3391  pofun  4312  poinxp  4695  ssimaex  5577  fndmdif  5621  dffo4  5664  fcompt  5686  fconst2g  5731  foco2  5754  foeqcnvco  5790  f1eqcocnv  5791  fliftel1  5794  isores3  5815  acexmid  5873  tfrlemi14d  6333  tfrcl  6364  dom2lem  6771  fiintim  6927  ordiso2  7033  mkvprop  7155  lt2addnq  7402  lt2mulnq  7403  ltexnqq  7406  genpdf  7506  addnqprl  7527  addnqpru  7528  addlocpr  7534  recexprlemopl  7623  caucvgsrlemgt1  7793  add4  8116  cnegex  8133  ltleadd  8401  zextle  9342  peano5uzti  9359  fnn0ind  9367  xrlttr  9793  xaddass  9867  iccshftr  9992  iccshftl  9994  iccdil  9996  icccntr  9998  fzaddel  10056  fzrev  10081  exbtwnzlemshrink  10246  seq3val  10455  iseqf1olemab  10486  exp3vallem  10518  mulexp  10556  expadd  10559  expmul  10562  leexp1a  10572  bccl  10742  hashfacen  10811  ovshftex  10823  2shfti  10835  caucvgre  10985  cvg1nlemcau  10988  resqrexlemcvg  11023  cau3lem  11118  rexico  11225  iooinsup  11280  climmpt  11303  subcn2  11314  climrecvg1n  11351  climcvg1nlem  11352  climcaucn  11354  mertenslem2  11539  eftlcl  11691  reeftlcl  11692  dvdsext  11855  sqoddm1div8z  11885  bezoutlemaz  11998  bezoutr1  12028  dvdslcm  12063  lcmeq0  12065  lcmcl  12066  lcmneg  12068  lcmdvds  12073  coprmgcdb  12082  dvdsprime  12116  pc2dvds  12323  prmpwdvds  12347  infpnlem1  12351  1arith  12359  mhmco  12828  mhmima  12829  dfgrp2  12856  mulgfng  12941  subgintm  13011  cnco  13614  cnss1  13619  tx2cn  13663  upxp  13665  metss  13887  txmetcnp  13911  cncfss  13963  cosz12  14094  bj-findis  14613