NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  exp3a GIF version

Theorem exp3a 425
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1 (φ → ((ψ χ) → θ))
Assertion
Ref Expression
exp3a (φ → (ψ → (χθ)))

Proof of Theorem exp3a
StepHypRef Expression
1 exp3a.1 . . . 4 (φ → ((ψ χ) → θ))
21com12 27 . . 3 ((ψ χ) → (φθ))
32ex 423 . 2 (ψ → (χ → (φθ)))
43com3r 73 1 (φ → (ψ → (χθ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  expdimp  426  pm3.3  431  syland  467  exp32  588  exp4c  591  exp4d  592  exp42  594  exp44  596  exp5c  599  impl  603  mpan2d  655  3impib  1149  exp5o  1170  exbir  1365  exp3acom3r  1370  exp3acom23  1372  nfsb4t  2080  ax11indn  2195  mo  2226  mopick  2266  ralrimivv  2705  mob2  3016  reuind  3039  reupick3  3540  pwadjoin  4119  opkthg  4131  nndisjeq  4429  ssfin  4470  ncfinraise  4481  sfin112  4529  sfintfin  4532  vfinspss  4551  phi11lem1  4595  funcnvuni  5161  fnun  5189  fconst5  5455  funfvima  5459  funsi  5520  fnpprod  5843  clos1conn  5879  trrd  5925  enprmaplem3  6078  nclenn  6249  ncslesuc  6267  nmembers1lem2  6269  nchoicelem17  6305  frecxp  6314  fnfrec  6320
  Copyright terms: Public domain W3C validator