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  7198  fimax2gtrilemstep  7205  cnegexlem3  8505  cnegex  8506  lemul12b  9194  climshftlemg  12086  prodeq2  12342  fprodmodd  12426  lcmdvds  12875  pwbdvdslemn  12962  dfgrp3mlem  13954  tgcl  15217  metss  15647  mpomulcn  15719  ivthinclemlr  15790  ivthinclemur  15792  nnnninfex  17187