Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  expd 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  759  3impib  1102  exp5o  1123  biassdc  1286  exbir  1325  expcomd  1330  expdcom  1331  mopick  1978  ralrimivv  2400  mob2  2721  reuind  2744  difin  3174  reupick3  3222  suctr  4158  tfisi  4310  relop  4486  funcnvuni  4968  fnun  5005  mpteqb  5261  funfvima  5390  poxp  5853  nnmass  6066  axprecex  6954  ltnsym  7104  nn0lt2  8322  fzind  8353  fnn0ind  8354  btwnz  8357  lbzbi  8551  ledivge1le  8652  elfz0ubfz0  8982  elfzo0z  9040  fzofzim  9044  flqeqceilz  9160  leexp2r  9308  bernneq  9369  cau3lem  9710  climuni  9814  mulcn2  9833  algcvgblem  9888
 Copyright terms: Public domain W3C validator