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	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrl	⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 286	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

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  7661  ltexnqq  7671  genprndl  7784  genprndu  7785  ltpopr  7858  ltsopr  7859  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemfl  7872  ltexprlemfu  7874  mulcmpblnrlemg  8003  cnegexlem2  8397  muladd  8605  eqord1  8705  eqord2  8706  divadddivap  8949  ltmul12a  9082  lemul12b  9083  cju  9183  zextlt  9616  supinfneg  9873  infsupneg  9874  xrre  10099  ixxdisj  10182  iooshf  10231  icodisj  10271  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  iccf1o  10284  fzaddel  10339  fzsubel  10340  seq3caopr  10803  seqcaoprg  10804  expineg2  10856  expsubap  10895  expnbnd  10971  facndiv  11047  hashfacen  11146  ccatpfx  11331  swrdccatfn  11354  swrdccatin2  11359  fprodeq0  12241  lcmdvds  12714  hashdvds  12856  eulerthlemh  12866  pceu  12931  pcqcl  12942  infpnlem1  12995  4sqlem11  13037  mhmpropd  13612  subsubm  13629  grplcan  13708  grplmulf1o  13720  dfgrp3mlem  13744  mulgfng  13774  mulgsubcl  13786  subsubg  13847  eqger  13874  resghm  13910  conjghm  13926  subsubrng  14292  subsubrg  14323  psrbagconf1o  14757  psrgrp  14769  txlm  15073  blininf  15218  xmeter  15230  xmetresbl  15234  limcimo  15459  dvdsppwf1o  15786  fsumdvdsmul  15788  sgmmul  15793  clwwlkn1loopb  16344