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

Theorem ad5antr 726
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 724 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 462 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  728  catass  14607  catpropd  14631  cidpropd  14632  monpropd  14659  funcpropd  14793  fucpropd  14870  drsdirfi  15091  neitr  18626  xkoccn  19034  trust  19646  restutopopn  19655  ucncn  19702  trcfilu  19711  ulmcau  21745  tgcgrxfr  22851  tgbtwnconn1  22883  legov  22892  f1otrg  22940  pthdepisspth  23296  omndmul2  25999  lgamucov  26872  heicant  28270  mblfinlem3  28274  mblfinlem4  28275  itg2gt0cn  28291  pell1234qrdich  29047
  Copyright terms: Public domain W3C validator