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

Theorem ad5antr 731
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 729 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 463 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad6antr  733  catass  15175  catpropd  15197  cidpropd  15198  monpropd  15225  funcpropd  15388  fucpropd  15465  drsdirfi  15766  mhmmnd  16391  neitr  19848  xkoccn  20286  trust  20898  restutopopn  20907  ucncn  20954  trcfilu  20963  ulmcau  22956  tgcgrxfr  24110  tgbtwnconn1  24163  legov  24173  legso  24186  midexlem  24270  perpneq  24292  footex  24296  colperpexlem3  24307  colperpex  24308  opphllem  24310  opphllem3  24322  lmieu  24351  f1otrg  24376  pthdepisspth  24778  omndmul2  27936  fimaproj  28071  qtophaus  28074  locfinreflem  28078  lgamucov  28844  heicant  30289  mblfinlem3  30293  mblfinlem4  30294  itg2gt0cn  30310  sstotbnd2  30510  pell1234qrdich  31036  icccncfext  31929  etransclem35  32291
  Copyright terms: Public domain W3C validator