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  2649  euotd  4283  peano5  4695  oelim  6549  lemul12a  9630  uzwo  10297  uzwoOLD  10298  catidd  13598  grpinveu  14532  2ndcctbss  17197  grporcan  20904  grpoinveu  20905  spansncvi  22247  sumdmdii  23011  glmrngo  25585  cmpmon  25918  unichnidl  26759  hbtlem2  27431  elfznelfzo  28213  injresinj  28215  ad4ant13  28519  ad4ant14  28520  ad4ant123  28521  ad4ant124  28522  ad4ant134  28523  ad4ant23  28524  ad4ant24  28525  ad4ant234  28526  ad5ant12  28527  ad5ant13  28528  ad5ant14  28529  ad5ant15  28530  ad5ant23  28531  ad5ant24  28532  ad5ant25  28533  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  ad5ant123  28537  ad5ant124  28538  ad5ant125  28539  ad5ant134  28540  ad5ant135  28541  ad5ant145  28542  ad5ant1345  28543  ad5ant2345  28544  linepsubN  30563  pmapsub  30579  cdlemkid4  31745
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