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

Theorem ad4antr 714
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 712 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 453 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad5antr  716  prdsval  13683  catass  13916  catpropd  13940  cidpropd  13941  subccocl  14047  funcco  14073  natpropd  14178  fucpropd  14179  prfval  14301  xpcpropd  14310  acsfiindd  14608  neitr  17249  hauscmplem  17474  trcfilu  18329  cfilucfilOLD  18604  cfilucfil  18605  restmetu  18622  metucnOLD  18623  metucn  18624  cnheibor  18985  dvlip2  19884  eupatrl  21695  esumcst  24460  lgamucov  24827  cvmlift3lem2  25012  mblfinlem3  26257  mblfinlem4  26258  itg2addnclem2  26271  itg2gt0cn  26274  ftc1cnnc  26293  ftc1anc  26302  nn0prpwlem  26339  sstotbnd2  26497  pell1234qrdich  26938  pell14qrdich  26946  pell1qrgap  26951  climrec  27719  climsuse  27724  2cshwmod  28291  3cyclfrgra  28479  2spot0  28527  lcfl8  32374
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 179  df-an 362
  Copyright terms: Public domain W3C validator