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  5330  fundmen  7485  fiint  7691  ltexprlem6  9313  divgt0  10300  divge0  10301  le2sq2  12044  iscatd  14715  isfuncd  14879  islmodd  17062  lmodvsghm  17114  islssd  17125  basis2  18674  neindisj  18839  dvidlem  21508  spansneleq  25110  elspansn4  25113  adjmul  25633  kbass6  25662  mdsl0  25851  chirredlem1  25931  rngonegmn1r  28896  3dim1  33419  linepsubN  33704  pmapsub  33720
  Copyright terms: Public domain W3C validator