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 185  df-an 371
This theorem is referenced by:  imp43  595  pm2.61da3ne  2768  onmindif  4908  oaordex  7099  pssnn  7634  alephval3  8383  dfac5  8401  dfac2  8403  coftr  8545  zorn2lem6  8773  addcanpi  9171  mulcanpi  9172  ltmpi  9176  ltexprlem6  9313  axpre-sup  9439  bndndx  10681  dmdprdd  16588  lssssr  17142  evl1gsumdlem  17901  1stcrest  19175  mdsymlem3  25946  mdsymlem6  25949  sumdmdlem  25959  prtlem17  29161  coe1fzgsumdlem  30981  cvratlem  33373  paddidm  33793  pmodlem2  33799  pclfinclN  33902
  Copyright terms: Public domain W3C validator