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

Theorem ad4antlr 738
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 736 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 467 1  |-  ( ( ( ( ( ch 
/\  ph )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  ad5antlr  740  initoeu2  15904  cpmatacl  19732  cpmatmcllem  19734  cpmatmcl  19735  chfacfisf  19870  chfacfisfcpmat  19871  restcld  20180  pthaus  20645  txhaus  20654  xkohaus  20660  alexsubALTlem4  21057  ustuqtop3  21250  ulmcau  23342  usgra2wlkspth  25341  clwlkisclwwlklem1  25507  usg2spot2nb  25785  locfinreflem  28669  cmpcref  28679  pstmxmet  28702  sigapildsys  28986  ldgenpisyslem1  28987  nn0prpwlem  30977  poimirlem29  31927  heicant  31933  mblfinlem3  31937  mblfinlem4  31938  itg2addnclem2  31952  itg2gt0cn  31955  ftc1cnnc  31974  sstotbnd2  32064  pell1234qrdich  35671  jm2.26lem3  35820  cvgdvgrat  36564  icccncfext  37629  fourierdlem34  37868  fourierdlem87  37921  etransclem35  37998  bgoldbwt  38634  bgoldbtbnd  38660  ply1mulgsumlem2  39523  nn0sumshdiglemA  39774
  Copyright terms: Public domain W3C validator