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

Theorem imp4b 574
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 573 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp43  579  onmindif  4664  oaordex  6794  pssnn  7320  alephval3  7984  dfac5  8002  dfac2  8004  coftr  8146  zorn2lem6  8374  addcanpi  8769  mulcanpi  8770  ltmpi  8774  ltexprlem6  8911  axpre-sup  9037  bndndx  10213  dmdprdd  15553  lssssr  16022  1stcrest  17509  mdsymlem3  23901  mdsymlem6  23904  sumdmdlem  23914  prtlem17  26717  cvratlem  30156  paddidm  30576  pmodlem2  30582  pclfinclN  30685
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 178  df-an 361
  Copyright terms: Public domain W3C validator