Theorem adantrl 478

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 110	. 2 |- ( ( th /\ ps ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 286	1 |- ( ( ph /\ ( th /\ 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:  ad2ant2l  508  ad2ant2rl  511  3ad2antr2  1187  3ad2antr3  1188  xordidc  1441  foco  5559  fvun1  5700  isocnv  5935  isores2  5937  f1oiso2  5951  offval  6226  xp2nd  6312  1stconst  6367  2ndconst  6368  tfrlem9  6465  nnmordi  6662  dom2lem  6923  fundmen  6959  mapen  7007  ssenen  7012  ltsonq  7585  ltexnqq  7595  genprndl  7708  genprndu  7709  ltpopr  7782  ltsopr  7783  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemdisj  7793  ltexprlemfl  7796  ltexprlemfu  7798  mulcmpblnrlemg  7927  cnegexlem2  8322  muladd  8530  eqord1  8630  eqord2  8631  divadddivap  8874  ltmul12a  9007  lemul12b  9008  cju  9108  zextlt  9539  supinfneg  9790  infsupneg  9791  xrre  10016  ixxdisj  10099  iooshf  10148  icodisj  10188  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  iccf1o  10200  fzaddel  10255  fzsubel  10256  seq3caopr  10717  seqcaoprg  10718  expineg2  10770  expsubap  10809  expnbnd  10885  facndiv  10961  hashfacen  11058  ccatpfx  11233  swrdccatfn  11256  swrdccatin2  11261  fprodeq0  12128  lcmdvds  12601  hashdvds  12743  eulerthlemh  12753  pceu  12818  pcqcl  12829  infpnlem1  12882  4sqlem11  12924  mhmpropd  13499  subsubm  13516  grplcan  13595  grplmulf1o  13607  dfgrp3mlem  13631  mulgfng  13661  mulgsubcl  13673  subsubg  13734  eqger  13761  resghm  13797  conjghm  13813  subsubrng  14178  subsubrg  14209  psrgrp  14649  txlm  14953  blininf  15098  xmeter  15110  xmetresbl  15114  limcimo  15339  dvdsppwf1o  15663  fsumdvdsmul  15665  sgmmul  15670