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

Theorem imp4b 594
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
imp4b  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)

Proof of Theorem imp4b
StepHypRef Expression
1 imp4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21imp4a 593 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32imp 431 1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  imp43  599  pm2.61da3ne  2745  onmindif  5529  oaordex  7265  pssnn  7794  alephval3  8543  dfac5  8561  dfac2  8563  coftr  8705  zorn2lem6  8933  addcanpi  9326  mulcanpi  9327  ltmpi  9331  ltexprlem6  9468  axpre-sup  9595  bndndx  10870  relexpaddd  13111  dmdprdd  17624  lssssr  18169  coe1fzgsumdlem  18888  evl1gsumdlem  18937  1stcrest  20460  mdsymlem3  28050  mdsymlem6  28053  sumdmdlem  28063  mclsax  30209  mclsppslem  30223  prtlem17  32372  cvratlem  32911  paddidm  33331  pmodlem2  33337  pclfinclN  33440  icceuelpart  38468
  Copyright terms: Public domain W3C validator