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

Theorem ad3antlr 462
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antlr  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad2antlr 458 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 261 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad4antlr  464  phpm  6327  phplem4on  6329  fidifsnen  6331  fisbth  6340  fin0  6342  fin0or  6343  prmuloc  6664  cauappcvgprlemopl  6744  cauappcvgprlemdisj  6749  cauappcvgprlemladdfl  6753  caucvgprlemopl  6767  axcaucvglemcau  6972  ssfzo12bi  9081  rebtwn2zlemstep  9107  btwnzge0  9142  cjap  9506  caucvgre  9580
  Copyright terms: Public domain W3C validator