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  7099  ctssdclemn0  7108  cauappcvgprlemladdfu  7652  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlemlim  7679  caucvgprprlemml  7692  caucvgprprlemloc  7701  caucvgprprlemlim  7709  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemloc  7719  suplocsrlem  7806  axcaucvglemres  7897  nn0ltexp2  10685  resqrexlemglsq  11026  xrmaxifle  11249  xrmaxiflemlub  11251  divalglemeuneg  11922  bezoutlemnewy  11991  ctiunctlemfo  12434  mhmmnd  12934  txmetcnp  13911  mulcncf  13984  suplociccreex  13995  cnplimclemr  14031  limccnpcntop  14037  lgsval  14298
  Copyright terms: Public domain W3C validator