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  1166  3ad2antr3  1167  xordidc  1419  foco  5511  fvun1  5647  isocnv  5882  isores2  5884  f1oiso2  5898  offval  6168  xp2nd  6254  1stconst  6309  2ndconst  6310  tfrlem9  6407  nnmordi  6604  dom2lem  6865  fundmen  6900  mapen  6945  ssenen  6950  ltsonq  7513  ltexnqq  7523  genprndl  7636  genprndu  7637  ltpopr  7710  ltsopr  7711  ltexprlemm  7715  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemdisj  7721  ltexprlemfl  7724  ltexprlemfu  7726  mulcmpblnrlemg  7855  cnegexlem2  8250  muladd  8458  eqord1  8558  eqord2  8559  divadddivap  8802  ltmul12a  8935  lemul12b  8936  cju  9036  zextlt  9467  supinfneg  9718  infsupneg  9719  xrre  9944  ixxdisj  10027  iooshf  10076  icodisj  10116  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  iccf1o  10128  fzaddel  10183  fzsubel  10184  seq3caopr  10642  seqcaoprg  10643  expineg2  10695  expsubap  10734  expnbnd  10810  facndiv  10886  hashfacen  10983  ccatpfx  11155  fprodeq0  11961  lcmdvds  12434  hashdvds  12576  eulerthlemh  12586  pceu  12651  pcqcl  12662  infpnlem1  12715  4sqlem11  12757  mhmpropd  13331  subsubm  13348  grplcan  13427  grplmulf1o  13439  dfgrp3mlem  13463  mulgfng  13493  mulgsubcl  13505  subsubg  13566  eqger  13593  resghm  13629  conjghm  13645  subsubrng  14009  subsubrg  14040  psrgrp  14480  txlm  14784  blininf  14929  xmeter  14941  xmetresbl  14945  limcimo  15170  dvdsppwf1o  15494  fsumdvdsmul  15496  sgmmul  15501