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

Theorem ad4antr 712
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 710 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 451 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad5antr  714  prdsval  13371  catass  13604  catpropd  13628  cidpropd  13629  subccocl  13735  funcco  13761  funcpropd  13790  natpropd  13866  fucpropd  13867  prfval  13989  xpcpropd  13998  acsfiindd  14296  esumcst  23451  itg2addnclem2  25004  itg2gt0cn  25006  ftc1cnnc  25025  climrec  27832  climsuse  27837  eupatrl  28385  3cyclfrgra  28437
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 177  df-an 360
  Copyright terms: Public domain W3C validator