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

Theorem ad5antr 740
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad5antr  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad4antr 738 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 467 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  ad6antr  742  catass  15592  catpropd  15614  cidpropd  15615  monpropd  15642  funcpropd  15805  fucpropd  15882  drsdirfi  16183  mhmmnd  16808  neitr  20196  xkoccn  20634  trust  21244  restutopopn  21253  ucncn  21300  trcfilu  21309  ulmcau  23350  lgamucov  23963  tgcgrxfr  24563  tgbtwnconn1  24620  legov  24630  legso  24644  midexlem  24737  perpneq  24759  footex  24763  colperpexlem3  24774  colperpex  24775  opphllem  24777  opphllem3  24791  outpasch  24797  hlpasch  24798  lmieu  24826  trgcopy  24846  trgcopyeu  24848  dfcgra2  24871  acopyeu  24875  cgrg3col4  24884  f1otrg  24901  pthdepisspth  25304  omndmul2  28475  fimaproj  28660  qtophaus  28663  locfinreflem  28667  heicant  31975  mblfinlem3  31979  mblfinlem4  31980  itg2gt0cn  31997  sstotbnd2  32106  pell1234qrdich  35707  supxrgelem  37560  icccncfext  37765  etransclem35  38134  pthdepissPth  39695
  Copyright terms: Public domain W3C validator