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

Theorem imp43 580
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 575 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32imp 420 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  sotriOLD  5267  fundmen  7181  fiint  7384  ltexprlem6  8919  divgt0  9879  divge0  9880  le2sq2  11458  iscatd  13899  isfuncd  14063  luble  14439  glble  14444  spwmo  14659  islmodd  15957  lmodvsghm  16006  islssd  16013  basis2  17017  neindisj  17182  dvidlem  19803  spansneleq  23073  elspansn4  23076  adjmul  23596  kbass6  23625  mdsl0  23814  chirredlem1  23894  rngonegmn1r  26567  3dim1  30265  linepsubN  30550  pmapsub  30566
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 179  df-an 362
  Copyright terms: Public domain W3C validator