MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antlr Unicode version

Theorem ad3antlr 711
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 707 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 451 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad4antlr  713  mreexexlem4d  13565  2ndcdisj  17198  lmdvg  23391  gsumpropd2lem  23394  ltflcei  24998  lxflflp1  25000  itg2addnclem2  25004  itg2gt0cn  25006  ftc1cnnc  25025  wallispilem3  27919  fargshiftfva  28384  eupatrl  28385  constr3trllem2  28397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator