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

Theorem expd 245
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1 (φ → ((ψ χ) → θ))
Assertion
Ref Expression
expd (φ → (ψ → (χθ)))

Proof of Theorem expd
StepHypRef Expression
1 exp3a.1 . . . 4 (φ → ((ψ χ) → θ))
21com12 27 . . 3 ((ψ χ) → (φθ))
32ex 108 . 2 (ψ → (χ → (φθ)))
43com3r 73 1 (φ → (ψ → (χθ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  expdimp  246  pm3.3  248  syland  277  exp32  347  exp4c  350  exp4d  351  exp42  353  exp44  355  exp5c  358  impl  362  mpan2d  404  pm2.6dc  758  3impib  1101  exp5o  1122  biassdc  1283  exbir  1322  expcomd  1327  expdcom  1328  mopick  1975  ralrimivv  2394  mob2  2715  reuind  2738  difin  3168  reupick3  3216  suctr  4124  tfisi  4253  relop  4429  funcnvuni  4911  fnun  4948  mpteqb  5204  funfvima  5333  poxp  5794  nnmass  6005  axprecex  6764  ltnsym  6901  nn0lt2  8098  fzind  8129  fnn0ind  8130  btwnz  8133  lbzbi  8327  elfz0ubfz0  8752  elfzo0z  8810  fzofzim  8814  leexp2r  8962  bernneq  9022
  Copyright terms: Public domain W3C validator