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

Theorem ad6antr 735
Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1
Assertion
Ref Expression
ad6antr

Proof of Theorem ad6antr
StepHypRef Expression
1 ad2ant.1 . . 3
21ad5antr 733 . 2
32adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  ad7antr  737  catass  15083  funcpropd  15269  natpropd  15345  restutop  20740  utopreg  20755  restmetu  21090  istrkgcb  23853  tgifscgr  23900  tgbtwnconn1lem3  23961  legtrd  23976  miriso  24050  footex  24095  opphllem3  24121  opphl  24125  f1otrge  24175  cusgrares  24472  clwlkisclwwlklem1  24787  lgamucov  28580  heicant  30049  mblfinlem3  30053  limclner  31657
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
  Copyright terms: Public domain W3C validator