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  4813  foco  5629  fvun1  5772  isocnv  6020  isores2  6022  f1oiso2  6036  offval  6314  xp2nd  6404  1stconst  6461  2ndconst  6462  tfrlem9  6594  nnmordi  6793  dom2lem  7062  fundmen  7098  mapen  7150  mapunen  7155  ssenen  7156  ltsonq  7771  ltexnqq  7781  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemfl  7982  ltexprlemfu  7984  mulcmpblnrlemg  8113  cnegexlem2  8509  muladd  8718  eqord1  8818  eqord2  8819  divadddivap  9065  ltmul12a  9198  lemul12b  9199  cju  9299  zextlt  9749  supinfneg  10011  infsupneg  10012  xrre  10239  ixxdisj  10322  iooshf  10371  icodisj  10411  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  iccf1o  10424  fzaddel  10482  fzsubel  10483  seq3caopr  10953  seqcaoprg  10954  expineg2  11006  expsubap  11045  expnbnd  11122  facndiv  11199  hashfibclem  11304  hashfacen  11306  hashf1lem1  11307  ccatpfx  11495  swrdccatfn  11518  swrdccatin2  11523  fprodeq0  12409  lcmdvds  12882  hashdvds  13028  eulerthlemh  13038  pceu  13103  pcqcl  13114  infpnlem1  13167  4sqlem11  13209  mhmpropd  13832  subsubm  13849  grplcan  13926  grplmulf1o  13938  dfgrp3mlem  13962  mulgfng  13986  mulgsubcl  13998  subsubg  14059  eqger  14086  resghm  14122  conjghm  14138  subsubrng  14631  subsubrg  14662  issubassa2  15144  psrbagconf1o  15174  psrgrp  15195  txlm  15505  blininf  15650  xmeter  15662  xmetresbl  15666  limcimo  15891  dvdsppwf1o  16283  fsumdvdsmul  16285  sgmmul  16290  bposlem6  16316  clwwlkn1loopb  16866