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

Theorem imp3a 420
 Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1 (φ → (ψ → (χθ)))
Assertion
Ref Expression
imp3a (φ → ((ψ χ) → θ))

Proof of Theorem imp3a
StepHypRef Expression
1 imp3.1 . . . 4 (φ → (ψ → (χθ)))
21com3l 75 . . 3 (ψ → (χ → (φθ)))
32imp 418 . 2 ((ψ χ) → (φθ))
43com12 27 1 (φ → ((ψ χ) → θ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  imp32  422  pm3.31  432  syland  467  imp4c  574  imp4d  575  imp5d  582  expimpd  586  expl  601  3expib  1154  equs5  1996  sbied  2036  rsp2  2676  moi  3019  reu6  3025  sbciegft  3076  pwadjoin  4119  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  ssfin  4470  tfinltfinlem1  4500  evenodddisj  4516  spfininduct  4540  vfinspss  4551  iss  5000  funssres  5144  fv3  5341  tz6.12-1  5344  funfvima  5459  funsi  5520  fnpprod  5843  fundmen  6043  enprmaplem6  6081  leltctr  6212  nchoicelem6  6294  nchoicelem17  6305  fnfrec  6320
 Copyright terms: Public domain W3C validator