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  4768  foco  5579  fvun1  5721  isocnv  5962  isores2  5964  f1oiso2  5978  offval  6252  xp2nd  6338  1stconst  6395  2ndconst  6396  tfrlem9  6528  nnmordi  6727  dom2lem  6988  fundmen  7024  mapen  7075  ssenen  7080  ltsonq  7678  ltexnqq  7688  genprndl  7801  genprndu  7802  ltpopr  7875  ltsopr  7876  ltexprlemm  7880  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemdisj  7886  ltexprlemfl  7889  ltexprlemfu  7891  mulcmpblnrlemg  8020  cnegexlem2  8414  muladd  8622  eqord1  8722  eqord2  8723  divadddivap  8966  ltmul12a  9099  lemul12b  9100  cju  9200  zextlt  9633  supinfneg  9890  infsupneg  9891  xrre  10116  ixxdisj  10199  iooshf  10248  icodisj  10288  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  iccf1o  10301  fzaddel  10356  fzsubel  10357  seq3caopr  10820  seqcaoprg  10821  expineg2  10873  expsubap  10912  expnbnd  10988  facndiv  11064  hashfacen  11163  ccatpfx  11348  swrdccatfn  11371  swrdccatin2  11376  fprodeq0  12258  lcmdvds  12731  hashdvds  12873  eulerthlemh  12883  pceu  12948  pcqcl  12959  infpnlem1  13012  4sqlem11  13054  mhmpropd  13629  subsubm  13646  grplcan  13725  grplmulf1o  13737  dfgrp3mlem  13761  mulgfng  13791  mulgsubcl  13803  subsubg  13864  eqger  13891  resghm  13927  conjghm  13943  subsubrng  14309  subsubrg  14340  psrbagconf1o  14774  psrgrp  14786  txlm  15090  blininf  15235  xmeter  15247  xmetresbl  15251  limcimo  15476  dvdsppwf1o  15803  fsumdvdsmul  15805  sgmmul  15810  clwwlkn1loopb  16361