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  7284  ctssdclemn0  7293  cauappcvgprlemladdfu  7857  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprlemlim  7884  caucvgprprlemml  7897  caucvgprprlemloc  7906  caucvgprprlemlim  7914  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemloc  7924  suplocsrlem  8011  axcaucvglemres  8102  nn0ltexp2  10948  resqrexlemglsq  11554  xrmaxifle  11778  xrmaxiflemlub  11780  divalglemeuneg  12455  bezoutlemnewy  12538  4sqlemsdc  12944  ctiunctlemfo  13031  mhmmnd  13674  txmetcnp  15213  mulcncf  15303  suplociccreex  15319  cnplimclemr  15364  limccnpcntop  15370  lgsval  15704