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  5494  fvun1  5630  isocnv  5861  isores2  5863  f1oiso2  5877  offval  6147  xp2nd  6233  1stconst  6288  2ndconst  6289  tfrlem9  6386  nnmordi  6583  dom2lem  6840  fundmen  6874  mapen  6916  ssenen  6921  ltsonq  7482  ltexnqq  7492  genprndl  7605  genprndu  7606  ltpopr  7679  ltsopr  7680  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemfl  7693  ltexprlemfu  7695  mulcmpblnrlemg  7824  cnegexlem2  8219  muladd  8427  eqord1  8527  eqord2  8528  divadddivap  8771  ltmul12a  8904  lemul12b  8905  cju  9005  zextlt  9435  supinfneg  9686  infsupneg  9687  xrre  9912  ixxdisj  9995  iooshf  10044  icodisj  10084  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  iccf1o  10096  fzaddel  10151  fzsubel  10152  seq3caopr  10604  seqcaoprg  10605  expineg2  10657  expsubap  10696  expnbnd  10772  facndiv  10848  hashfacen  10945  fprodeq0  11799  lcmdvds  12272  hashdvds  12414  eulerthlemh  12424  pceu  12489  pcqcl  12500  infpnlem1  12553  4sqlem11  12595  mhmpropd  13168  subsubm  13185  grplcan  13264  grplmulf1o  13276  dfgrp3mlem  13300  mulgfng  13330  mulgsubcl  13342  subsubg  13403  eqger  13430  resghm  13466  conjghm  13482  subsubrng  13846  subsubrg  13877  psrgrp  14313  txlm  14599  blininf  14744  xmeter  14756  xmetresbl  14760  limcimo  14985  dvdsppwf1o  15309  fsumdvdsmul  15311  sgmmul  15316