Theorem adantll 473

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 109	. 2 |- ( ( th /\ ph ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 281	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antlr  486  ad2ant2l  505  ad2ant2lr  507  ad5ant23  519  ad5ant24  520  ad5ant25  521  3ad2antl3  1156  3adant1l  1225  reu6  2919  sbc2iegf  3025  sbcralt  3031  sbcrext  3032  indifdir  3383  pofun  4297  poinxp  4680  ssimaex  5557  fndmdif  5601  dffo4  5644  fcompt  5666  fconst2g  5711  foco2  5733  foeqcnvco  5769  f1eqcocnv  5770  fliftel1  5773  isores3  5794  acexmid  5852  tfrlemi14d  6312  tfrcl  6343  dom2lem  6750  fiintim  6906  ordiso2  7012  mkvprop  7134  lt2addnq  7366  lt2mulnq  7367  ltexnqq  7370  genpdf  7470  addnqprl  7491  addnqpru  7492  addlocpr  7498  recexprlemopl  7587  caucvgsrlemgt1  7757  add4  8080  cnegex  8097  ltleadd  8365  zextle  9303  peano5uzti  9320  fnn0ind  9328  xrlttr  9752  xaddass  9826  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzaddel  10015  fzrev  10040  exbtwnzlemshrink  10205  seq3val  10414  iseqf1olemab  10445  exp3vallem  10477  mulexp  10515  expadd  10518  expmul  10521  leexp1a  10531  bccl  10701  hashfacen  10771  ovshftex  10783  2shfti  10795  caucvgre  10945  cvg1nlemcau  10948  resqrexlemcvg  10983  cau3lem  11078  rexico  11185  iooinsup  11240  climmpt  11263  subcn2  11274  climrecvg1n  11311  climcvg1nlem  11312  climcaucn  11314  mertenslem2  11499  eftlcl  11651  reeftlcl  11652  dvdsext  11815  sqoddm1div8z  11845  bezoutlemaz  11958  bezoutr1  11988  dvdslcm  12023  lcmeq0  12025  lcmcl  12026  lcmneg  12028  lcmdvds  12033  coprmgcdb  12042  dvdsprime  12076  pc2dvds  12283  prmpwdvds  12307  infpnlem1  12311  1arith  12319  mhmco  12705  mhmima  12706  dfgrp2  12732  cnco  13015  cnss1  13020  tx2cn  13064  upxp  13066  metss  13288  txmetcnp  13312  cncfss  13364  cosz12  13495  bj-findis  14014