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

Theorem ad4antlr 732
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 730 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 465 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  734  restcld  18781  pthaus  19216  txhaus  19225  xkohaus  19231  alexsubALTlem4  19627  ustuqtop3  19823  ulmcau  21865  pstmxmet  26329  heicant  28431  mblfinlem3  28435  mblfinlem4  28436  itg2addnclem2  28449  itg2gt0cn  28452  ftc1cnnc  28471  nn0prpwlem  28522  sstotbnd2  28678  jm2.26lem3  29355  usgra2wlkspth  30303  clwlkisclwwlklem1  30454  usg2spot2nb  30663  ply1mulgsumlem2  30850  pmatcollpw1dst  30906
  Copyright terms: Public domain W3C validator