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:  fundmen  7608  fiint  7815  ltexprlem6  9436  divgt0  10431  divge0  10432  le2sq2  12245  iscatd  15089  isfuncd  15280  islmodd  17644  lmodvsghm  17697  islssd  17708  basis2  19578  neindisj  19744  dvidlem  22444  spansneleq  26614  elspansn4  26617  adjmul  27137  kbass6  27166  mdsl0  27355  chirredlem1  27435  rngonegmn1r  30515  3dim1  35292  linepsubN  35577  pmapsub  35593
  Copyright terms: Public domain W3C validator