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

Theorem ad5antr 487
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 485 . 2 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
32adantr 274 1 ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad6antr  489  difinfinf  6954  ctssdclemn0  6963  cauappcvgprlemladdfu  7430  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlemlim  7457  caucvgprprlemml  7470  caucvgprprlemloc  7479  caucvgprprlemlim  7487  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemloc  7497  suplocsrlem  7584  axcaucvglemres  7675  resqrexlemglsq  10762  xrmaxifle  10983  xrmaxiflemlub  10985  divalglemeuneg  11547  bezoutlemnewy  11611  ctiunctlemfo  11879  txmetcnp  12614  mulcncf  12687  suplociccreex  12698  cnplimclemr  12734  limccnpcntop  12740
  Copyright terms: Public domain W3C validator