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

Theorem expd 254
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 113 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
43com3r 78 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  expdimp  255  pm3.3  257  syland  287  exp32  357  exp4c  360  exp4d  361  exp42  363  exp44  365  exp5c  368  impl  372  mpan2d  419  pm2.6dc  795  3impib  1139  exp5o  1160  biassdc  1329  exbir  1368  expcomd  1373  expdcom  1374  mopick  2023  ralrimivv  2450  mob2  2786  reuind  2809  difin  3225  reupick3  3273  suctr  4222  tfisi  4375  relop  4554  funcnvuni  5048  fnun  5085  mpteqb  5356  funfvima  5487  poxp  5954  nnmass  6202  supisoti  6649  axprecex  7359  ltnsym  7515  nn0lt2  8761  fzind  8794  fnn0ind  8795  btwnz  8798  lbzbi  9033  ledivge1le  9135  elfz0ubfz0  9464  elfzo0z  9523  fzofzim  9527  flqeqceilz  9653  leexp2r  9908  bernneq  9971  cau3lem  10443  climuni  10576  mulcn2  10595  dvdsabseq  10730  ndvdssub  10812  bezoutlemmain  10869  rplpwr  10898  algcvgblem  10913  euclemma  11007
  Copyright terms: Public domain W3C validator