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

Theorem imp43 595
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 590 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32imp 429 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  sotriOLD  5405  fundmen  7601  fiint  7809  ltexprlem6  9431  divgt0  10422  divge0  10423  le2sq2  12223  iscatd  14945  isfuncd  15109  islmodd  17389  lmodvsghm  17442  islssd  17453  basis2  19321  neindisj  19486  dvidlem  22187  spansneleq  26311  elspansn4  26314  adjmul  26834  kbass6  26863  mdsl0  27052  chirredlem1  27132  rngonegmn1r  30280  3dim1  34664  linepsubN  34949  pmapsub  34965
  Copyright terms: Public domain W3C validator