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

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

Proof of Theorem ad6antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad5antr 745 . 2  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
32adantr 471 1  |-  ( ( ( ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  /\  si )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad7antr  749  catass  15641  funcpropd  15854  natpropd  15930  restutop  21301  utopreg  21316  restmetu  21634  lgamucov  24012  istrkgcb  24553  tgifscgr  24602  tgbtwnconn1lem3  24668  legtrd  24683  miriso  24764  footex  24812  opphllem3  24840  opphl  24845  trgcopy  24895  cgratr  24914  dfcgra2  24920  inaghl  24930  cgrg3col4  24933  f1otrge  24951  cusgrares  25249  clwlkisclwwlklem1  25564  heicant  32020  mblfinlem3  32024  limclner  37770  hoidmvle  38460
  Copyright terms: Public domain W3C validator