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 )

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  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4809  foco  5624  fvun1  5766  isocnv  6010  isores2  6012  f1oiso2  6026  offval  6303  xp2nd  6393  1stconst  6450  2ndconst  6451  tfrlem9  6583  nnmordi  6782  dom2lem  7051  fundmen  7087  mapen  7139  mapunen  7144  ssenen  7145  ltsonq  7758  ltexnqq  7768  genprndl  7881  genprndu  7882  ltpopr  7955  ltsopr  7956  ltexprlemm  7960  ltexprlemopl  7961  ltexprlemopu  7963  ltexprlemdisj  7966  ltexprlemfl  7969  ltexprlemfu  7971  mulcmpblnrlemg  8100  cnegexlem2  8495  muladd  8704  eqord1  8804  eqord2  8805  divadddivap  9050  ltmul12a  9183  lemul12b  9184  cju  9284  zextlt  9720  supinfneg  9977  infsupneg  9978  xrre  10204  ixxdisj  10287  iooshf  10336  icodisj  10376  iccshftr  10378  iccshftl  10380  iccdil  10382  icccntr  10384  iccf1o  10389  fzaddel  10446  fzsubel  10447  seq3caopr  10913  seqcaoprg  10914  expineg2  10966  expsubap  11005  expnbnd  11082  facndiv  11158  hashfibclem  11263  hashfacen  11265  hashf1lem1  11266  ccatpfx  11454  swrdccatfn  11477  swrdccatin2  11482  fprodeq0  12365  lcmdvds  12838  hashdvds  12980  eulerthlemh  12990  pceu  13055  pcqcl  13066  infpnlem1  13119  4sqlem11  13161  mhmpropd  13753  subsubm  13770  grplcan  13847  grplmulf1o  13859  dfgrp3mlem  13883  mulgfng  13907  mulgsubcl  13919  subsubg  13980  eqger  14007  resghm  14043  conjghm  14059  subsubrng  14498  subsubrg  14529  psrbagconf1o  14990  psrgrp  15002  txlm  15306  blininf  15451  xmeter  15463  xmetresbl  15467  limcimo  15692  dvdsppwf1o  16020  fsumdvdsmul  16022  sgmmul  16027  clwwlkn1loopb  16578