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

Theorem imp4b 590
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 589 . 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 187  df-an 371
This theorem is referenced by:  imp43  595  pm2.61da3ne  2725  onmindif  5501  oaordex  7246  pssnn  7775  alephval3  8525  dfac5  8543  dfac2  8545  coftr  8687  zorn2lem6  8915  addcanpi  9309  mulcanpi  9310  ltmpi  9314  ltexprlem6  9451  axpre-sup  9578  bndndx  10837  relexpaddd  13038  dmdprdd  17352  lssssr  17921  coe1fzgsumdlem  18665  evl1gsumdlem  18714  1stcrest  20248  mdsymlem3  27750  mdsymlem6  27753  sumdmdlem  27763  mclsax  29794  mclsppslem  29808  prtlem17  31912  cvratlem  32451  paddidm  32871  pmodlem2  32877  pclfinclN  32980  icceuelpart  37716
  Copyright terms: Public domain W3C validator