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

Theorem expd 249
 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 112 . 2 (𝜓 → (𝜒 → (𝜑𝜃)))
43com3r 77 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105 This theorem is referenced by:  expdimp  250  pm3.3  252  syland  281  exp32  351  exp4c  354  exp4d  355  exp42  357  exp44  359  exp5c  362  impl  366  mpan2d  412  pm2.6dc  770  3impib  1113  exp5o  1134  biassdc  1302  exbir  1341  expcomd  1346  expdcom  1347  mopick  1994  ralrimivv  2417  mob2  2743  reuind  2766  difin  3201  reupick3  3249  suctr  4185  tfisi  4337  relop  4513  funcnvuni  4995  fnun  5032  mpteqb  5288  funfvima  5417  poxp  5880  nnmass  6096  supisoti  6413  axprecex  7011  ltnsym  7162  nn0lt2  8379  fzind  8411  fnn0ind  8412  btwnz  8415  lbzbi  8647  ledivge1le  8749  elfz0ubfz0  9083  elfzo0z  9141  fzofzim  9145  flqeqceilz  9267  leexp2r  9473  bernneq  9536  cau3lem  9940  climuni  10044  mulcn2  10063  dvdsabseq  10158  algcvgblem  10257
 Copyright terms: Public domain W3C validator