Theorem adantrl 467

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
adantrl	|- ( ( ph /\ ( th /\ ps ) ) -> ch )

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 109	. 2 |- ( ( th /\ ps ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 282	1 |- ( ( ph /\ ( th /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad2ant2l  497  ad2ant2rl  500  3ad2antr2  1130  3ad2antr3  1131  xordidc  1360  foco  5313  fvun1  5441  isocnv  5666  isores2  5668  f1oiso2  5682  offval  5943  xp2nd  6018  1stconst  6072  2ndconst  6073  tfrlem9  6170  nnmordi  6366  dom2lem  6620  fundmen  6654  mapen  6693  ssenen  6698  ltsonq  7151  ltexnqq  7161  genprndl  7274  genprndu  7275  ltpopr  7348  ltsopr  7349  ltexprlemm  7353  ltexprlemopl  7354  ltexprlemopu  7356  ltexprlemdisj  7359  ltexprlemfl  7362  ltexprlemfu  7364  mulcmpblnrlemg  7480  cnegexlem2  7858  muladd  8062  eqord1  8161  eqord2  8162  divadddivap  8397  ltmul12a  8525  lemul12b  8526  cju  8626  zextlt  9044  supinfneg  9289  infsupneg  9290  xrre  9493  ixxdisj  9576  iooshf  9625  icodisj  9665  iccshftr  9667  iccshftl  9669  iccdil  9671  icccntr  9673  iccf1o  9677  fzaddel  9729  fzsubel  9730  seq3caopr  10146  expineg2  10192  expsubap  10231  expnbnd  10305  facndiv  10375  hashfacen  10469  lcmdvds  11603  hashdvds  11739  txlm  12287  blininf  12410  xmeter  12422  xmetresbl  12426  limcimo  12587