Theorem adantrl 447

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  ad2ant2l  477  ad2ant2rl  480  3ad2antr2  1070  3ad2antr3  1071  xordidc  1290  foco  5116  fvun1  5239  isocnv  5451  isores2  5453  f1oiso2  5466  offval  5719  xp2nd  5793  1stconst  5842  2ndconst  5843  tfrlem9  5935  nnmordi  6089  dom2lem  6252  fundmen  6286  ltsonq  6496  ltexnqq  6506  genprndl  6619  genprndu  6620  ltpopr  6693  ltsopr  6694  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemfl  6707  ltexprlemfu  6709  mulcmpblnrlemg  6825  cnegexlem2  7187  muladd  7381  divadddivap  7703  ltmul12a  7826  lemul12b  7827  cju  7913  zextlt  8332  xrre  8733  ixxdisj  8772  iooshf  8821  icodisj  8860  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  iccf1o  8872  fzaddel  8922  fzsubel  8923  iseqcaopr  9242  expineg2  9264  expsubap  9302  expnbnd  9372