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

Theorem ad6antr 735
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 733 . 2  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
32adantr 465 1  |-  ( ( ( ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  /\  si )  ->  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:  ad7antr  737  catass  14622  funcpropd  14808  natpropd  14884  restutop  19810  utopreg  19825  restmetu  20160  tgifscgr  22959  tgcgrxfr  22968  tgbtwnconn1lem3  23004  legtrd  23018  miriso  23071  footex  23107  f1otrge  23116  cusgrares  23378  lgamucov  27022  heicant  28423  mblfinlem3  28427  clwlkisclwwlklem1  30446
  Copyright terms: Public domain W3C validator