Theorem adantrl 469

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad2ant2l  499  ad2ant2rl  502  3ad2antr2  1147  3ad2antr3  1148  xordidc  1377  foco  5355  fvun1  5487  isocnv  5712  isores2  5714  f1oiso2  5728  offval  5989  xp2nd  6064  1stconst  6118  2ndconst  6119  tfrlem9  6216  nnmordi  6412  dom2lem  6666  fundmen  6700  mapen  6740  ssenen  6745  ltsonq  7206  ltexnqq  7216  genprndl  7329  genprndu  7330  ltpopr  7403  ltsopr  7404  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemfl  7417  ltexprlemfu  7419  mulcmpblnrlemg  7548  cnegexlem2  7938  muladd  8146  eqord1  8245  eqord2  8246  divadddivap  8487  ltmul12a  8618  lemul12b  8619  cju  8719  zextlt  9143  supinfneg  9390  infsupneg  9391  xrre  9603  ixxdisj  9686  iooshf  9735  icodisj  9775  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  iccf1o  9787  fzaddel  9839  fzsubel  9840  seq3caopr  10256  expineg2  10302  expsubap  10341  expnbnd  10415  facndiv  10485  hashfacen  10579  lcmdvds  11760  hashdvds  11897  txlm  12448  blininf  12593  xmeter  12605  xmetresbl  12609  limcimo  12803