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  362  exp4c  365  exp4d  366  exp42  368  exp44  370  exp5c  373  impl  377  mpan2d  424  a2and  532  pm2.6dc  832  3impib  1164  exp5o  1189  biassdc  1358  exbir  1397  expcomd  1402  expdcom  1403  mopick  2055  ralrimivv  2490  mob2  2837  reuind  2862  difin  3283  reupick3  3331  suctr  4313  tfisi  4471  relop  4659  funcnvuni  5162  fnun  5199  mpteqb  5479  funfvima  5617  poxp  6097  nnmass  6351  supisoti  6865  axprecex  7656  ltnsym  7818  nn0lt2  9100  fzind  9134  fnn0ind  9135  btwnz  9138  lbzbi  9376  ledivge1le  9481  elfz0ubfz0  9870  elfzo0z  9929  fzofzim  9933  flqeqceilz  10059  leexp2r  10315  bernneq  10380  cau3lem  10854  climuni  11030  mulcn2  11049  dvdsabseq  11472  ndvdssub  11554  bezoutlemmain  11613  rplpwr  11642  algcvgblem  11657  euclemma  11751  basis2  12142  txcnp  12367  metcnp3  12607
  Copyright terms: Public domain W3C validator