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

Theorem imp4a 572
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
imp4a  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )

Proof of Theorem imp4a
StepHypRef Expression
1 imp4.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
2 impexp 433 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ibr 218 1  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp4b  573  imp4d  575  imp55  584  imp511  585  reuss2  3461  wefrc  4403  f1oweALT  5867  riotasvdOLD  6364  tfrlem1  6407  tfrlem9  6417  tz7.49  6473  oaordex  6572  dfac2  7773  zorn2lem4  8142  zorn2lem7  8145  psslinpr  8671  facwordi  11318  ndvdssub  12622  elcls  16826  elcls3  16836  neibl  18063  met2ndc  18085  itgcn  19213  branmfn  22701  atcvatlem  22981  atcvat4i  22993  and4as  25042  prtlem15  26846  pmtrfrn  27503  cvlsupr4  30157  cvlsupr5  30158  cvlsupr6  30159  2llnneN  30220  cvrat4  30254  llnexchb2  30680  cdleme48gfv1  31347  cdlemg6e  31433  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dihglblem5apreN  32103  dihglbcpreN  32112
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