Theorem adantrl 470

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 284	1 |- ( ( ph /\ ( th /\ 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:  ad2ant2l  500  ad2ant2rl  503  3ad2antr2  1153  3ad2antr3  1154  xordidc  1389  foco  5420  fvun1  5552  isocnv  5779  isores2  5781  f1oiso2  5795  offval  6057  xp2nd  6134  1stconst  6189  2ndconst  6190  tfrlem9  6287  nnmordi  6484  dom2lem  6738  fundmen  6772  mapen  6812  ssenen  6817  ltsonq  7339  ltexnqq  7349  genprndl  7462  genprndu  7463  ltpopr  7536  ltsopr  7537  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemdisj  7547  ltexprlemfl  7550  ltexprlemfu  7552  mulcmpblnrlemg  7681  cnegexlem2  8074  muladd  8282  eqord1  8381  eqord2  8382  divadddivap  8623  ltmul12a  8755  lemul12b  8756  cju  8856  zextlt  9283  supinfneg  9533  infsupneg  9534  xrre  9756  ixxdisj  9839  iooshf  9888  icodisj  9928  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  iccf1o  9940  fzaddel  9994  fzsubel  9995  seq3caopr  10418  expineg2  10464  expsubap  10503  expnbnd  10578  facndiv  10652  hashfacen  10749  fprodeq0  11558  lcmdvds  12011  hashdvds  12153  eulerthlemh  12163  pceu  12227  pcqcl  12238  infpnlem1  12289  txlm  12919  blininf  13064  xmeter  13076  xmetresbl  13080  limcimo  13274