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

Theorem ad3antlr 477
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 473 . 2 (((𝜒𝜑) ∧ 𝜃) → 𝜓)
32adantr 270 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad4antlr  479  phpm  6533  phplem4on  6535  fidifsnen  6538  fisbth  6551  fin0  6553  fin0or  6554  fisseneq  6592  djudom  6731  enomnilem  6738  prmuloc  7069  cauappcvgprlemopl  7149  cauappcvgprlemdisj  7154  cauappcvgprlemladdfl  7158  caucvgprlemopl  7172  axcaucvglemcau  7377  ssfzo12bi  9564  rebtwn2zlemstep  9592  btwnzge0  9635  addmodlteq  9733  frecuzrdgg  9751  hashxp  10130  cjap  10235  caucvgre  10309  minmax  10554  sumeq2  10638  bezoutlemmain  10862  dfgcd2  10878  lcmgcdlem  10934  peano4nninf  11334  nninfalllemn  11336
  Copyright terms: Public domain W3C validator