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

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

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad4antr 731 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 465 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  ad6antr  735  catass  14616  catpropd  14640  cidpropd  14641  monpropd  14668  funcpropd  14802  fucpropd  14879  drsdirfi  15100  neitr  18764  xkoccn  19172  trust  19784  restutopopn  19793  ucncn  19840  trcfilu  19849  ulmcau  21840  tgcgrxfr  22950  tgbtwnconn1  22987  legov  22996  midexlem  23063  perpneq  23081  f1otrg  23085  pthdepisspth  23441  omndmul2  26143  lgamucov  26993  heicant  28397  mblfinlem3  28401  mblfinlem4  28402  itg2gt0cn  28418  pell1234qrdich  29173
  Copyright terms: Public domain W3C validator