Theorem ad5antr 496

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

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad5antr	⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad4antr 494	. 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
3	2	adantr 276	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:  ad6antr  498  difinfinf  7305  ctssdclemn0  7314  cauappcvgprlemladdfu  7879  caucvgprlemloc  7900  caucvgprlemladdfu  7902  caucvgprlemlim  7906  caucvgprprlemml  7919  caucvgprprlemloc  7928  caucvgprprlemlim  7936  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemloc  7946  suplocsrlem  8033  axcaucvglemres  8124  nn0ltexp2  10977  resqrexlemglsq  11605  xrmaxifle  11829  xrmaxiflemlub  11831  divalglemeuneg  12507  bezoutlemnewy  12590  4sqlemsdc  12996  ctiunctlemfo  13083  mhmmnd  13726  txmetcnp  15271  mulcncf  15361  suplociccreex  15377  cnplimclemr  15422  limccnpcntop  15428  lgsval  15762