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

Theorem ad4antlr 731
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 729 . 2  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
32adantr 463 1  |-  ( ( ( ( ( ch 
/\  ph )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad5antlr  733  initoeu2  15619  cpmatacl  19509  cpmatmcllem  19511  cpmatmcl  19512  chfacfisf  19647  chfacfisfcpmat  19648  restcld  19966  pthaus  20431  txhaus  20440  xkohaus  20446  alexsubALTlem4  20842  ustuqtop3  21038  ulmcau  23082  usgra2wlkspth  25038  clwlkisclwwlklem1  25204  usg2spot2nb  25482  locfinreflem  28296  cmpcref  28306  pstmxmet  28329  sigapildsys  28610  ldgenpisyslem1  28611  nn0prpwlem  30550  heicant  31421  mblfinlem3  31425  mblfinlem4  31426  itg2addnclem2  31440  itg2gt0cn  31443  ftc1cnnc  31462  sstotbnd2  31552  pell1234qrdich  35158  jm2.26lem3  35305  cvgdvgrat  36042  icccncfext  37058  fourierdlem34  37291  fourierdlem87  37344  etransclem35  37420  bgoldbwt  37831  bgoldbtbnd  37857  ply1mulgsumlem2  38498  nn0sumshdiglemA  38750
  Copyright terms: Public domain W3C validator