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

Theorem imp41 576
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
imp41  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )

Proof of Theorem imp41
StepHypRef Expression
1 imp4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21imp 418 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  ( th  ->  ta ) ) )
32imp31 421 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  3anassrs  1173  ralrimivvva  2636  euotd  4267  peano5  4679  oelim  6533  lemul12a  9614  uzwo  10281  uzwoOLD  10282  catidd  13582  grpinveu  14516  2ndcctbss  17181  grporcan  20888  grpoinveu  20889  spansncvi  22231  sumdmdii  22995  glmrngo  25482  cmpmon  25815  unichnidl  26656  hbtlem2  27328  linepsubN  29941  pmapsub  29957  cdlemkid4  31123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator