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

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

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3
21ad4antr 731 . 2
32adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  ad6antr  735  catass  15083  catpropd  15104  cidpropd  15105  monpropd  15132  funcpropd  15269  fucpropd  15346  drsdirfi  15567  mhmmnd  16192  neitr  19681  xkoccn  20120  trust  20732  restutopopn  20741  ucncn  20788  trcfilu  20797  ulmcau  22790  tgcgrxfr  23909  tgbtwnconn1  23962  legov  23972  legso  23985  midexlem  24069  perpneq  24091  footex  24095  colperpexlem3  24106  colperpex  24107  opphllem  24109  opphllem3  24121  lmieu  24150  f1otrg  24174  pthdepisspth  24576  omndmul2  27702  fimaproj  27836  qtophaus  27839  locfinreflem  27843  lgamucov  28580  heicant  30049  mblfinlem3  30053  mblfinlem4  30054  itg2gt0cn  30070  sstotbnd2  30270  pell1234qrdich  30797  icccncfext  31690  etransclem35  32052
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