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

Theorem ad4antr 713
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad4antr  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )

Proof of Theorem ad4antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad3antrrr 711 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 452 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad5antr  715  prdsval  13668  catass  13901  catpropd  13925  cidpropd  13926  subccocl  14032  funcco  14058  natpropd  14163  fucpropd  14164  prfval  14286  xpcpropd  14295  acsfiindd  14593  neitr  17234  hauscmplem  17459  trcfilu  18314  cfilucfilOLD  18589  cfilucfil  18590  restmetu  18607  metucnOLD  18608  metucn  18609  cnheibor  18970  dvlip2  19869  eupatrl  21680  esumcst  24445  lgamucov  24812  cvmlift3lem2  24997  mblfinlem2  26208  mblfinlem3  26209  itg2addnclem2  26220  itg2gt0cn  26223  ftc1cnnc  26242  nn0prpwlem  26279  sstotbnd2  26437  pell1234qrdich  26878  pell14qrdich  26886  pell1qrgap  26891  climrec  27660  climsuse  27665  2cshwmod  28187  3cyclfrgra  28306  2spot0  28354  lcfl8  32201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator