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

Theorem ad4antlr 744
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 742 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 471 1  |-  ( ( ( ( ( ch 
/\  ph )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad5antlr  746  initoeu2  15959  cpmatacl  19788  cpmatmcllem  19790  cpmatmcl  19791  chfacfisf  19926  chfacfisfcpmat  19927  restcld  20236  pthaus  20701  txhaus  20710  xkohaus  20716  alexsubALTlem4  21113  ustuqtop3  21306  ulmcau  23398  usgra2wlkspth  25397  clwlkisclwwlklem1  25563  usg2spot2nb  25841  locfinreflem  28715  cmpcref  28725  pstmxmet  28748  sigapildsys  29032  ldgenpisyslem1  29033  nn0prpwlem  31026  poimirlem29  32013  heicant  32019  mblfinlem3  32023  mblfinlem4  32024  itg2addnclem2  32038  itg2gt0cn  32041  ftc1cnnc  32060  sstotbnd2  32150  pell1234qrdich  35751  jm2.26lem3  35900  cvgdvgrat  36705  icccncfext  37802  fourierdlem34  38041  fourierdlem87  38094  etransclem35  38171  bgoldbwt  38915  bgoldbtbnd  38941  ply1mulgsumlem2  40451  nn0sumshdiglemA  40702
  Copyright terms: Public domain W3C validator