Theorem adantrl 482

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2ant2l  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4811  foco  5626  fvun1  5769  isocnv  6017  isores2  6019  f1oiso2  6033  offval  6310  xp2nd  6400  1stconst  6457  2ndconst  6458  tfrlem9  6590  nnmordi  6789  dom2lem  7058  fundmen  7094  mapen  7146  mapunen  7151  ssenen  7152  ltsonq  7765  ltexnqq  7775  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemfl  7976  ltexprlemfu  7978  mulcmpblnrlemg  8107  cnegexlem2  8502  muladd  8711  eqord1  8811  eqord2  8812  divadddivap  9057  ltmul12a  9190  lemul12b  9191  cju  9291  zextlt  9738  supinfneg  9995  infsupneg  9996  xrre  10222  ixxdisj  10305  iooshf  10354  icodisj  10394  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  iccf1o  10407  fzaddel  10465  fzsubel  10466  seq3caopr  10932  seqcaoprg  10933  expineg2  10985  expsubap  11024  expnbnd  11101  facndiv  11177  hashfibclem  11282  hashfacen  11284  hashf1lem1  11285  ccatpfx  11473  swrdccatfn  11496  swrdccatin2  11501  fprodeq0  12384  lcmdvds  12857  hashdvds  12999  eulerthlemh  13009  pceu  13074  pcqcl  13085  infpnlem1  13138  4sqlem11  13180  mhmpropd  13773  subsubm  13790  grplcan  13867  grplmulf1o  13879  dfgrp3mlem  13903  mulgfng  13927  mulgsubcl  13939  subsubg  14000  eqger  14027  resghm  14063  conjghm  14079  subsubrng  14522  subsubrg  14553  issubassa2  15035  psrbagconf1o  15064  psrgrp  15076  txlm  15380  blininf  15525  xmeter  15537  xmetresbl  15541  limcimo  15766  dvdsppwf1o  16103  fsumdvdsmul  16105  sgmmul  16110  clwwlkn1loopb  16661