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  1163  3ad2antr3  1164  xordidc  1399  foco  5448  fvun1  5582  isocnv  5811  isores2  5813  f1oiso2  5827  offval  6089  xp2nd  6166  1stconst  6221  2ndconst  6222  tfrlem9  6319  nnmordi  6516  dom2lem  6771  fundmen  6805  mapen  6845  ssenen  6850  ltsonq  7396  ltexnqq  7406  genprndl  7519  genprndu  7520  ltpopr  7593  ltsopr  7594  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemdisj  7604  ltexprlemfl  7607  ltexprlemfu  7609  mulcmpblnrlemg  7738  cnegexlem2  8132  muladd  8340  eqord1  8439  eqord2  8440  divadddivap  8683  ltmul12a  8816  lemul12b  8817  cju  8917  zextlt  9344  supinfneg  9594  infsupneg  9595  xrre  9819  ixxdisj  9902  iooshf  9951  icodisj  9991  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  iccf1o  10003  fzaddel  10058  fzsubel  10059  seq3caopr  10482  expineg2  10528  expsubap  10567  expnbnd  10643  facndiv  10718  hashfacen  10815  fprodeq0  11624  lcmdvds  12078  hashdvds  12220  eulerthlemh  12230  pceu  12294  pcqcl  12305  infpnlem1  12356  mhmpropd  12856  grplcan  12931  grplmulf1o  12943  dfgrp3mlem  12967  mulgfng  12986  mulgsubcl  12996  subsubg  13055  eqger  13081  subsubrg  13364  txlm  13749  blininf  13894  xmeter  13906  xmetresbl  13910  limcimo  14104