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  4498  oaordex  6572  pssnn  7097  alephval3  7753  dfac5  7771  dfac2  7773  coftr  7915  zorn2lem6  8144  addcanpi  8539  mulcanpi  8540  ltmpi  8544  ltexprlem6  8681  axpre-sup  8807  bndndx  9980  dmdprdd  15253  lmodvsdi1OLD  15667  lssssr  15726  1stcrest  17195  mdsymlem3  23001  mdsymlem6  23004  sumdmdlem  23014  cmphmia  25901  cmphmib  25902  iri  25903  prtlem17  26847  cvratlem  30232  paddidm  30652  pmodlem2  30658  pclfinclN  30761
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