Theorem adantllr 485

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 406	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4ant13  517  ad4ant134  1248  ad5ant145  1275  r19.29an  2693  diffifi  7203  fimax2gtrilemstep  7210  cnegexlem3  8511  cnegex  8512  lemul12b  9200  climshftlemg  12094  prodeq2  12350  fprodmodd  12434  lcmdvds  12883  pwbdvdslemn  12970  dfgrp3mlem  13963  tgcl  15302  metss  15732  mpomulcn  15804  ivthinclemlr  15875  ivthinclemur  15877  nnnninfex  17283