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

Theorem imp4b 573
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 572 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp43  578  onmindif  4482  oaordex  6556  pssnn  7081  alephval3  7737  dfac5  7755  dfac2  7757  coftr  7899  zorn2lem6  8128  addcanpi  8523  mulcanpi  8524  ltmpi  8528  ltexprlem6  8665  axpre-sup  8791  bndndx  9964  dmdprdd  15237  lmodvsdi1OLD  15651  lssssr  15710  1stcrest  17179  mdsymlem3  22985  mdsymlem6  22988  sumdmdlem  22998  cmphmia  25798  cmphmib  25799  iri  25800  prtlem17  26744  cvratlem  29610  paddidm  30030  pmodlem2  30036  pclfinclN  30139
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 177  df-an 360
  Copyright terms: Public domain W3C validator