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

Theorem imp4a 573
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 434 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ibr 219 1  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp4b  574  imp4d  576  imp55  585  imp511  586  reuss2  3564  wefrc  4517  f1oweALT  6013  riotasvdOLD  6529  tfrlem1  6572  tfrlem9  6582  tz7.49  6638  oaordex  6737  dfac2  7944  zorn2lem4  8312  zorn2lem7  8315  psslinpr  8841  facwordi  11507  ndvdssub  12854  elcls  17060  elcls3  17070  neibl  18421  met2ndc  18443  itgcn  19601  branmfn  23456  atcvatlem  23736  atcvat4i  23748  prtlem15  26415  pmtrfrn  27069  cvlsupr4  29460  cvlsupr5  29461  cvlsupr6  29462  2llnneN  29523  cvrat4  29557  llnexchb2  29983  cdleme48gfv1  30650  cdlemg6e  30736  dihord6apre  31371  dihord5b  31374  dihord5apre  31377  dihglblem5apreN  31406  dihglbcpreN  31415
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