ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad5antr GIF version

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
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad4antr 494 . 2 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
32adantr 276 1 ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff set class
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  7103  ctssdclemn0  7112  cauappcvgprlemladdfu  7656  caucvgprlemloc  7677  caucvgprlemladdfu  7679  caucvgprlemlim  7683  caucvgprprlemml  7696  caucvgprprlemloc  7705  caucvgprprlemlim  7713  suplocexprlemmu  7720  suplocexprlemru  7721  suplocexprlemloc  7723  suplocsrlem  7810  axcaucvglemres  7901  nn0ltexp2  10692  resqrexlemglsq  11034  xrmaxifle  11257  xrmaxiflemlub  11259  divalglemeuneg  11931  bezoutlemnewy  12000  ctiunctlemfo  12443  mhmmnd  12986  txmetcnp  14158  mulcncf  14231  suplociccreex  14242  cnplimclemr  14278  limccnpcntop  14284  lgsval  14545
  Copyright terms: Public domain W3C validator