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  cpmatacl  18984  cpmatmcllem  18986  cpmatmcl  18987  chfacfisf  19122  chfacfisfcpmat  19123  restcld  19439  pthaus  19874  txhaus  19883  xkohaus  19889  alexsubALTlem4  20285  ustuqtop3  20481  ulmcau  22524  usgra2wlkspth  24297  clwlkisclwwlklem1  24463  usg2spot2nb  24742  pstmxmet  27512  heicant  29626  mblfinlem3  29630  mblfinlem4  29631  itg2addnclem2  29644  itg2gt0cn  29647  ftc1cnnc  29666  nn0prpwlem  29717  sstotbnd2  29873  jm2.26lem3  30547  icccncfext  31226  ply1mulgsumlem2  32060
  Copyright terms: Public domain W3C validator