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

Theorem expd 255
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 30 . . 3 ((𝜓𝜒) → (𝜑𝜃))
32ex 114 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
43com3r 79 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  expdimp  256  pm3.3  258  syland  288  exp32  358  exp4c  361  exp4d  362  exp42  364  exp44  366  exp5c  369  impl  373  mpan2d  420  a2and  526  pm2.6dc  798  3impib  1142  exp5o  1163  biassdc  1332  exbir  1371  expcomd  1376  expdcom  1377  mopick  2027  ralrimivv  2455  mob2  2796  reuind  2821  difin  3237  reupick3  3285  suctr  4257  tfisi  4415  relop  4599  funcnvuni  5096  fnun  5133  mpteqb  5406  funfvima  5540  poxp  6011  nnmass  6262  supisoti  6759  axprecex  7476  ltnsym  7632  nn0lt2  8889  fzind  8922  fnn0ind  8923  btwnz  8926  lbzbi  9162  ledivge1le  9264  elfz0ubfz0  9597  elfzo0z  9656  fzofzim  9660  flqeqceilz  9786  leexp2r  10070  bernneq  10135  cau3lem  10608  climuni  10742  mulcn2  10762  dvdsabseq  11187  ndvdssub  11269  bezoutlemmain  11326  rplpwr  11355  algcvgblem  11370  euclemma  11464  basis2  11807
  Copyright terms: Public domain W3C validator