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

Theorem ad5antr 485
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 483 . 2 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
32adantr 272 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  487  difinfinf  6952  ctssdclemn0  6961  cauappcvgprlemladdfu  7426  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprlemlim  7453  caucvgprprlemml  7466  caucvgprprlemloc  7475  caucvgprprlemlim  7483  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemloc  7493  suplocsrlem  7580  axcaucvglemres  7671  resqrexlemglsq  10734  xrmaxifle  10955  xrmaxiflemlub  10957  divalglemeuneg  11516  bezoutlemnewy  11580  ctiunctlemfo  11847  txmetcnp  12582  mulcncf  12655  cnplimclemr  12681  limccnpcntop  12687
  Copyright terms: Public domain W3C validator