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

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

Proof of Theorem ad4antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad3antlr 712 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 452 1  |-  ( ( ( ( ( ch 
/\  ph )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad5antlr  716  restcld  17236  pthaus  17670  txhaus  17679  xkohaus  17685  alexsubALTlem4  18081  ustuqtop3  18273  ulmcau  20311  pstmxmet  24292  mblfinlem3  26245  mblfinlem4  26246  itg2addnclem2  26257  itg2gt0cn  26260  ftc1cnnc  26279  nn0prpwlem  26325  sstotbnd2  26483  jm2.26lem3  27072  usgra2wlkspth  28308  usg2spot2nb  28454
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 178  df-an 361
  Copyright terms: Public domain W3C validator