Theorem adantrl 462

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 108	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 280	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  ad2ant2l  492  ad2ant2rl  495  3ad2antr2  1105  3ad2antr3  1106  xordidc  1331  foco  5141  fvun1  5265  isocnv  5476  isores2  5478  f1oiso2  5491  offval  5744  xp2nd  5818  1stconst  5867  2ndconst  5868  tfrlem9  5962  nnmordi  6148  dom2lem  6311  fundmen  6345  ltsonq  6639  ltexnqq  6649  genprndl  6762  genprndu  6763  ltpopr  6836  ltsopr  6837  ltexprlemm  6841  ltexprlemopl  6842  ltexprlemopu  6844  ltexprlemdisj  6847  ltexprlemfl  6850  ltexprlemfu  6852  mulcmpblnrlemg  6968  cnegexlem2  7340  muladd  7544  divadddivap  7871  ltmul12a  7994  lemul12b  7995  cju  8094  zextlt  8509  supinfneg  8753  infsupneg  8754  xrre  8952  ixxdisj  8991  iooshf  9040  icodisj  9079  iccshftr  9081  iccshftl  9083  iccdil  9085  icccntr  9087  iccf1o  9091  fzaddel  9142  fzsubel  9143  iseqcaopr  9547  expineg2  9571  expsubap  9610  expnbnd  9682  facndiv  9752  lcmdvds  10594