Theorem ad3antlr 480

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 476	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 272	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad4antlr  482  nntr2  6329  phpm  6688  phplem4on  6690  fidifsnen  6693  fisbth  6706  fin0  6708  fin0or  6709  fiintim  6746  fisseneq  6749  djudom  6893  difinfsnlem  6899  enomnilem  6922  prmuloc  7275  cauappcvgprlemopl  7355  cauappcvgprlemdisj  7360  cauappcvgprlemladdfl  7364  caucvgprlemopl  7378  axcaucvglemcau  7583  xaddf  9468  xleaddadd  9511  ssfzo12bi  9843  rebtwn2zlemstep  9871  btwnzge0  9914  addmodlteq  10012  frecuzrdgg  10030  hashxp  10413  cjap  10519  caucvgre  10593  minmax  10840  xrminmax  10873  sumeq2  10967  fsumconst  11062  bezoutlemmain  11479  dfgcd2  11495  lcmgcdlem  11551  cnpnei  12169  cnntr  12175  peano4nninf  12784  nninfalllemn  12786