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  5075  fundmen  6934  fiint  7133  ltexprlem6  8665  divgt0  9624  divge0  9625  le2sq2  11179  iscatd  13575  isfuncd  13739  luble  14115  glble  14120  spwmo  14335  islmodd  15633  lmodvsghm  15686  islssd  15693  basis2  16689  neindisj  16854  dvidlem  19265  spansneleq  22149  elspansn4  22152  adjmul  22672  kbass6  22701  mdsl0  22890  chirredlem1  22970  rngonegmn1r  26581  3dim1  29656  linepsubN  29941  pmapsub  29957
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