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

Theorem ad5antr 748
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 746 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 472 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  ad6antr  750  catass  15670  catpropd  15692  cidpropd  15693  monpropd  15720  funcpropd  15883  fucpropd  15960  drsdirfi  16261  mhmmnd  16886  neitr  20273  xkoccn  20711  trust  21322  restutopopn  21331  ucncn  21378  trcfilu  21387  ulmcau  23429  lgamucov  24042  tgcgrxfr  24642  tgbtwnconn1  24699  legov  24709  legso  24723  midexlem  24816  perpneq  24838  footex  24842  colperpexlem3  24853  colperpex  24854  opphllem  24856  opphllem3  24870  outpasch  24876  hlpasch  24877  lmieu  24905  trgcopy  24925  trgcopyeu  24927  dfcgra2  24950  acopyeu  24954  cgrg3col4  24963  f1otrg  24980  pthdepisspth  25383  omndmul2  28549  fimaproj  28734  qtophaus  28737  locfinreflem  28741  heicant  32039  mblfinlem3  32043  mblfinlem4  32044  itg2gt0cn  32061  sstotbnd2  32170  pell1234qrdich  35778  supxrgelem  37647  icccncfext  37862  etransclem35  38246  pthdepissPth  39927
  Copyright terms: Public domain W3C validator