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  14941  funcpropd  15127  natpropd  15203  restutop  20503  utopreg  20518  restmetu  20853  tgifscgr  23656  tgcgrxfr  23665  tgbtwnconn1lem3  23716  legtrd  23731  miriso  23791  footex  23831  mideulem  23841  f1otrge  23879  cusgrares  24176  clwlkisclwwlklem1  24491  lgamucov  28248  heicant  29654  mblfinlem3  29658  limclner  31221
  Copyright terms: Public domain W3C validator