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  14742  catpropd  14766  cidpropd  14767  monpropd  14794  funcpropd  14928  fucpropd  15005  drsdirfi  15226  neitr  18915  xkoccn  19323  trust  19935  restutopopn  19944  ucncn  19991  trcfilu  20000  ulmcau  21992  tgcgrxfr  23105  tgbtwnconn1  23143  legov  23153  midexlem  23228  perpneq  23249  footex  23253  colperplem3  23258  colperp  23259  mideulem  23260  f1otrg  23268  pthdepisspth  23624  omndmul2  26319  lgamucov  27167  heicant  28573  mblfinlem3  28577  mblfinlem4  28578  itg2gt0cn  28594  pell1234qrdich  29349
  Copyright terms: Public domain W3C validator