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

Theorem ad6antr 740
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 738 . 2  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
32adantr 466 1  |-  ( ( ( ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  /\  si )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad7antr  742  catass  15543  funcpropd  15756  natpropd  15832  restutop  21183  utopreg  21198  restmetu  21516  lgamucov  23828  istrkgcb  24367  tgifscgr  24416  tgbtwnconn1lem3  24479  legtrd  24494  miriso  24574  footex  24620  opphllem3  24648  opphl  24653  trgcopy  24702  cgratr  24721  dfcgra2  24726  f1otrge  24748  cusgrares  25045  clwlkisclwwlklem1  25360  heicant  31682  mblfinlem3  31686  limclner  37307
  Copyright terms: Public domain W3C validator