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

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

Proof of Theorem exp43
StepHypRef Expression
1 exp43.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
21ex 424 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32exp4b 591 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp53  601  funssres  5426  fvopab3ig  5735  fvmptt  5752  tfrlem2  6566  tfr3  6589  omordi  6738  odi  6751  nnmordi  6803  php  7220  fiint  7312  ordiso2  7410  cfcoflem  8078  zorn2lem5  8306  inar1  8576  psslinpr  8834  recexsrlem  8904  qaddcl  10515  qmulcl  10517  elfznelfzo  11112  expcan  11352  ltexp2  11353  bernneq  11425  expnbnd  11428  xpnnenOLD  12729  spwmo  14578  elcls3  17063  opnneissb  17094  txbas  17513  grpoidinvlem3  21635  grporcan  21650  shscli  22660  spansncol  22911  spanunsni  22922  spansncvi  22995  homco1  23145  homulass  23146  atomli  23726  chirredlem1  23734  cdj1i  23777  frinfm  26121  filbcmb  26126  unichnidl  26325  dmncan1  26370  pclfinclN  30115
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