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  1165  3ad2antr3  1166  xordidc  1410  foco  5491  fvun1  5627  isocnv  5858  isores2  5860  f1oiso2  5874  offval  6143  xp2nd  6224  1stconst  6279  2ndconst  6280  tfrlem9  6377  nnmordi  6574  dom2lem  6831  fundmen  6865  mapen  6907  ssenen  6912  ltsonq  7465  ltexnqq  7475  genprndl  7588  genprndu  7589  ltpopr  7662  ltsopr  7663  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemfl  7676  ltexprlemfu  7678  mulcmpblnrlemg  7807  cnegexlem2  8202  muladd  8410  eqord1  8510  eqord2  8511  divadddivap  8754  ltmul12a  8887  lemul12b  8888  cju  8988  zextlt  9418  supinfneg  9669  infsupneg  9670  xrre  9895  ixxdisj  9978  iooshf  10027  icodisj  10067  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  iccf1o  10079  fzaddel  10134  fzsubel  10135  seq3caopr  10587  seqcaoprg  10588  expineg2  10640  expsubap  10679  expnbnd  10755  facndiv  10831  hashfacen  10928  fprodeq0  11782  lcmdvds  12247  hashdvds  12389  eulerthlemh  12399  pceu  12464  pcqcl  12475  infpnlem1  12528  4sqlem11  12570  mhmpropd  13098  subsubm  13115  grplcan  13194  grplmulf1o  13206  dfgrp3mlem  13230  mulgfng  13254  mulgsubcl  13266  subsubg  13327  eqger  13354  resghm  13390  conjghm  13406  subsubrng  13770  subsubrg  13801  txlm  14515  blininf  14660  xmeter  14672  xmetresbl  14676  limcimo  14901  dvdsppwf1o  15225  fsumdvdsmul  15227  sgmmul  15232