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

Theorem ad4antlr 725
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 723 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 462 1  |-  ( ( ( ( ( ch 
/\  ph )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ad5antlr  727  restcld  18617  pthaus  19052  txhaus  19061  xkohaus  19067  alexsubALTlem4  19463  ustuqtop3  19659  ulmcau  21744  pstmxmet  26177  heicant  28267  mblfinlem3  28271  mblfinlem4  28272  itg2addnclem2  28285  itg2gt0cn  28288  ftc1cnnc  28307  nn0prpwlem  28358  sstotbnd2  28514  jm2.26lem3  29192  usgra2wlkspth  30141  clwlkisclwwlklem1  30292  usg2spot2nb  30501
  Copyright terms: Public domain W3C validator