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  13606  catass  13839  catpropd  13863  cidpropd  13864  subccocl  13970  funcco  13996  natpropd  14101  fucpropd  14102  prfval  14224  xpcpropd  14233  acsfiindd  14531  neitr  17167  hauscmplem  17392  trcfilu  18246  cfilucfil  18480  restmetu  18490  metucn  18491  cnheibor  18852  dvlip2  19747  eupatrl  21539  esumcst  24252  lgamucov  24602  cvmlift3lem2  24787  itg2addnclem2  25959  itg2gt0cn  25961  ftc1cnnc  25980  nn0prpwlem  26017  sstotbnd2  26175  pell1234qrdich  26616  pell14qrdich  26624  pell1qrgap  26629  climrec  27398  climsuse  27403  3cyclfrgra  27769  lcfl8  31618
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