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  1190  3ad2antr3  1191  xordidc  1444  opabssxpd  4788  foco  5603  fvun1  5745  isocnv  5986  isores2  5988  f1oiso2  6002  offval  6276  xp2nd  6362  1stconst  6419  2ndconst  6420  tfrlem9  6552  nnmordi  6751  dom2lem  7013  fundmen  7049  mapen  7101  mapunen  7106  ssenen  7107  ltsonq  7715  ltexnqq  7725  genprndl  7838  genprndu  7839  ltpopr  7912  ltsopr  7913  ltexprlemm  7917  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemdisj  7923  ltexprlemfl  7926  ltexprlemfu  7928  mulcmpblnrlemg  8057  cnegexlem2  8451  muladd  8659  eqord1  8759  eqord2  8760  divadddivap  9003  ltmul12a  9136  lemul12b  9137  cju  9237  zextlt  9673  supinfneg  9930  infsupneg  9931  xrre  10156  ixxdisj  10239  iooshf  10288  icodisj  10328  iccshftr  10330  iccshftl  10332  iccdil  10334  icccntr  10336  iccf1o  10341  fzaddel  10396  fzsubel  10397  seq3caopr  10861  seqcaoprg  10862  expineg2  10914  expsubap  10953  expnbnd  11029  facndiv  11105  hashfibclem  11210  hashfacen  11212  ccatpfx  11397  swrdccatfn  11420  swrdccatin2  11425  fprodeq0  12307  lcmdvds  12780  hashdvds  12922  eulerthlemh  12932  pceu  12997  pcqcl  13008  infpnlem1  13061  4sqlem11  13103  mhmpropd  13696  subsubm  13713  grplcan  13792  grplmulf1o  13804  dfgrp3mlem  13828  mulgfng  13858  mulgsubcl  13870  subsubg  13931  eqger  13958  resghm  13994  conjghm  14010  subsubrng  14376  subsubrg  14407  psrbagconf1o  14845  psrgrp  14857  txlm  15161  blininf  15306  xmeter  15318  xmetresbl  15322  limcimo  15547  dvdsppwf1o  15874  fsumdvdsmul  15876  sgmmul  15881  clwwlkn1loopb  16432