MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp4b 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  4611  oaordex  6737  pssnn  7263  alephval3  7924  dfac5  7942  dfac2  7944  coftr  8086  zorn2lem6  8314  addcanpi  8709  mulcanpi  8710  ltmpi  8714  ltexprlem6  8851  axpre-sup  8977  bndndx  10152  dmdprdd  15487  lssssr  15956  1stcrest  17437  mdsymlem3  23756  mdsymlem6  23759  sumdmdlem  23769  prtlem17  26416  cvratlem  29535  paddidm  29955  pmodlem2  29961  pclfinclN  30064
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