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

Theorem ad5antr 733
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 731 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 465 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  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:  ad6antr  735  catass  14955  catpropd  14976  cidpropd  14977  monpropd  15004  funcpropd  15138  fucpropd  15215  drsdirfi  15436  mhmmnd  16061  neitr  19547  xkoccn  19986  trust  20598  restutopopn  20607  ucncn  20654  trcfilu  20663  ulmcau  22655  tgcgrxfr  23774  tgbtwnconn1  23827  legov  23837  legso  23850  midexlem  23934  perpneq  23956  footex  23960  colperpexlem3  23971  colperpex  23972  opphllem  23974  opphllem3  23986  lmieu  24015  f1otrg  24039  pthdepisspth  24441  omndmul2  27568  fimaproj  27702  qtophaus  27705  locfinreflem  27709  lgamucov  28446  heicant  30017  mblfinlem3  30021  mblfinlem4  30022  itg2gt0cn  30038  sstotbnd2  30238  pell1234qrdich  30765  icccncfext  31593
  Copyright terms: Public domain W3C validator