ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  expd Unicode version

Theorem expd 256
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expd  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem expd
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 30 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 114 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 79 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  363  exp4c  366  exp4d  367  exp42  369  exp44  371  exp5c  374  impl  378  mpan2d  425  a2and  548  pm2.6dc  852  3impib  1190  exp5o  1215  biassdc  1384  exbir  1423  expcomd  1428  expdcom  1429  mopick  2091  ralrimivv  2545  mob2  2904  reuind  2929  difin  3357  reupick3  3405  suctr  4396  tfisi  4561  relop  4751  funcnvuni  5254  fnun  5291  mpteqb  5573  funfvima  5713  poxp  6194  nnmass  6449  supisoti  6969  axprecex  7815  ltnsym  7978  nn0lt2  9266  fzind  9300  fnn0ind  9301  btwnz  9304  lbzbi  9548  ledivge1le  9656  elfz0ubfz0  10054  elfzo0z  10113  fzofzim  10117  flqeqceilz  10247  leexp2r  10503  bernneq  10569  cau3lem  11050  climuni  11228  mulcn2  11247  dvdsabseq  11779  ndvdssub  11861  bezoutlemmain  11925  rplpwr  11954  algcvgblem  11975  euclemma  12072  basis2  12644  txcnp  12869  metcnp3  13109  bj-charfunr  13585
  Copyright terms: Public domain W3C validator