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

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

Proof of Theorem imp43
StepHypRef Expression
1 imp4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21imp4b 573 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32imp 418 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sotriOLD  5091  fundmen  6950  fiint  7149  ltexprlem6  8681  divgt0  9640  divge0  9641  le2sq2  11195  iscatd  13591  isfuncd  13755  luble  14131  glble  14136  spwmo  14351  islmodd  15649  lmodvsghm  15702  islssd  15709  basis2  16705  neindisj  16870  dvidlem  19281  spansneleq  22165  elspansn4  22168  adjmul  22688  kbass6  22717  mdsl0  22906  chirredlem1  22986  rngonegmn1r  26684  3dim1  30278  linepsubN  30563  pmapsub  30579
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