Theorem ad3antlr 476

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad2antlr 472	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 270	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:  ad4antlr  478  phpm  6351  phplem4on  6353  fidifsnen  6355  fisbth  6367  fin0  6369  fin0or  6370  prmuloc  6756  cauappcvgprlemopl  6836  cauappcvgprlemdisj  6841  cauappcvgprlemladdfl  6845  caucvgprlemopl  6859  axcaucvglemcau  7064  ssfzo12bi  9234  rebtwn2zlemstep  9261  btwnzge0  9302  addmodlteq  9400  cjap  9793  caucvgre  9867  minmax  10112  bezoutlemmain  10387  dfgcd2  10403  lcmgcdlem  10459