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  15103  funcpropd  15316  natpropd  15392  restutop  20866  utopreg  20881  restmetu  21216  istrkgcb  23979  tgifscgr  24026  tgbtwnconn1lem3  24087  legtrd  24102  miriso  24176  footex  24221  opphllem3  24247  opphl  24251  f1otrge  24302  cusgrares  24599  clwlkisclwwlklem1  24914  lgamucov  28777  heicant  30254  mblfinlem3  30258  limclner  31860
  Copyright terms: Public domain W3C validator