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

Theorem exp43 595
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 423 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32exp4b 590 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp53  600  funssres  5310  fvopab3ig  5615  fvmptt  5631  tfrlem2  6408  tfr3  6431  omordi  6580  odi  6593  nnmordi  6645  php  7061  fiint  7149  ordiso2  7246  cfcoflem  7914  zorn2lem5  8143  inar1  8413  psslinpr  8671  recexsrlem  8741  qaddcl  10348  qmulcl  10350  expcan  11170  ltexp2  11171  bernneq  11243  expnbnd  11246  xpnnenOLD  12504  spwmo  14351  elcls3  16836  opnneissb  16867  txbas  17278  grpoidinvlem3  20889  grporcan  20904  shscli  21912  spansncol  22163  spanunsni  22174  spansncvi  22247  homco1  22397  homulass  22398  atomli  22978  chirredlem1  22986  cdj1i  23029  cmpmon  25918  frinfm  26519  filbcmb  26535  unichnidl  26759  dmncan1  26804  elfznelfzo  28213  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