Theorem adantrl 461

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  491  ad2ant2rl  494  3ad2antr2  1104  3ad2antr3  1105  xordidc  1330  foco  5136  fvun1  5260  isocnv  5471  isores2  5473  f1oiso2  5486  offval  5739  xp2nd  5813  1stconst  5862  2ndconst  5863  tfrlem9  5958  nnmordi  6112  dom2lem  6275  fundmen  6309  ltsonq  6588  ltexnqq  6598  genprndl  6711  genprndu  6712  ltpopr  6785  ltsopr  6786  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemdisj  6796  ltexprlemfl  6799  ltexprlemfu  6801  mulcmpblnrlemg  6917  cnegexlem2  7284  muladd  7488  divadddivap  7815  ltmul12a  7938  lemul12b  7939  cju  8038  zextlt  8439  supinfneg  8683  infsupneg  8684  xrre  8887  ixxdisj  8926  iooshf  8975  icodisj  9014  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  iccf1o  9026  fzaddel  9077  fzsubel  9078  iseqcaopr  9462  expineg2  9485  expsubap  9524  expnbnd  9596  facndiv  9666  lcmdvds  10461