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

Theorem ad3antlr 470
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antlr ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad2antlr 466 . 2 (((𝜒𝜑) ∧ 𝜃) → 𝜓)
32adantr 265 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad4antlr  472  phpm  6358  phplem4on  6360  fidifsnen  6362  fisbth  6371  fin0  6373  fin0or  6374  prmuloc  6722  cauappcvgprlemopl  6802  cauappcvgprlemdisj  6807  cauappcvgprlemladdfl  6811  caucvgprlemopl  6825  axcaucvglemcau  7030  ssfzo12bi  9183  rebtwn2zlemstep  9209  btwnzge0  9250  addmodlteq  9348  cjap  9734  caucvgre  9808
  Copyright terms: Public domain W3C validator