Theorem adantllr 481

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantllr	⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 402	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:  ad4ant13  513  ad4ant134  1241  ad5ant145  1268  r19.29an  2673  diffifi  7078  fimax2gtrilemstep  7085  cnegexlem3  8349  cnegex  8350  lemul12b  9034  climshftlemg  11856  prodeq2  12111  fprodmodd  12195  lcmdvds  12644  pw2dvdslemn  12730  dfgrp3mlem  13674  tgcl  14781  metss  15211  mpomulcn  15283  ivthinclemlr  15354  ivthinclemur  15356  nnnninfex  16574