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  2787  onmindif  4967  oaordex  7204  pssnn  7735  alephval3  8487  dfac5  8505  dfac2  8507  coftr  8649  zorn2lem6  8877  addcanpi  9273  mulcanpi  9274  ltmpi  9278  ltexprlem6  9415  axpre-sup  9542  bndndx  10790  dmdprdd  16821  lssssr  17382  coe1fzgsumdlem  18114  evl1gsumdlem  18163  1stcrest  19720  mdsymlem3  27000  mdsymlem6  27003  sumdmdlem  27013  prtlem17  30221  cvratlem  34217  paddidm  34637  pmodlem2  34643  pclfinclN  34746
  Copyright terms: Public domain W3C validator