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

Theorem expd 256
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-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  362  exp4c  365  exp4d  366  exp42  368  exp44  370  exp5c  373  impl  377  mpan2d  424  a2and  547  pm2.6dc  847  3impib  1179  exp5o  1204  biassdc  1373  exbir  1412  expcomd  1417  expdcom  1418  mopick  2077  ralrimivv  2513  mob2  2864  reuind  2889  difin  3313  reupick3  3361  suctr  4343  tfisi  4501  relop  4689  funcnvuni  5192  fnun  5229  mpteqb  5511  funfvima  5649  poxp  6129  nnmass  6383  supisoti  6897  axprecex  7695  ltnsym  7857  nn0lt2  9139  fzind  9173  fnn0ind  9174  btwnz  9177  lbzbi  9415  ledivge1le  9520  elfz0ubfz0  9909  elfzo0z  9968  fzofzim  9972  flqeqceilz  10098  leexp2r  10354  bernneq  10419  cau3lem  10893  climuni  11069  mulcn2  11088  dvdsabseq  11551  ndvdssub  11633  bezoutlemmain  11692  rplpwr  11721  algcvgblem  11736  euclemma  11830  basis2  12224  txcnp  12449  metcnp3  12689
  Copyright terms: Public domain W3C validator