MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad4antr 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  13641  catass  13874  catpropd  13898  cidpropd  13899  subccocl  14005  funcco  14031  natpropd  14136  fucpropd  14137  prfval  14259  xpcpropd  14268  acsfiindd  14566  neitr  17206  hauscmplem  17431  trcfilu  18285  cfilucfilOLD  18560  cfilucfil  18561  restmetu  18578  metucnOLD  18579  metucn  18580  cnheibor  18941  dvlip2  19840  eupatrl  21651  esumcst  24416  lgamucov  24783  cvmlift3lem2  24968  mblfinlem2  26152  mblfinlem3  26153  itg2addnclem2  26164  itg2gt0cn  26167  ftc1cnnc  26186  nn0prpwlem  26223  sstotbnd2  26381  pell1234qrdich  26822  pell14qrdich  26830  pell1qrgap  26835  climrec  27604  climsuse  27609  3cyclfrgra  28127  2spot0  28175  lcfl8  31997
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