Theorem expcom 424

Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
exp.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
expcom	⊢ (ψ → (φ → χ))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 ⊢ ((φ ∧ ψ) → χ)
2	1	ex 423	. 2 ⊢ (φ → (ψ → χ))
3	2	com12 27	1 ⊢ (ψ → (φ → χ))

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:  ancoms  439  syldan  456  sylan  457  4casesdan  916  dedlema  920  dedlemb  921  dvelimv  1939  cbval2  2004  cbvex2  2005  2moswap  2279  2mos  2283  2eu2  2285  pm2.61ne  2591  r19.21be  2715  uneqdifeq  3638  ssunsn2  3865  ssuni  3913  uniss2  3922  elpwuni  4053  lenltfin  4469  tfincl  4492  tfinltfin  4501  evenoddnnnul  4514  nnadjoin  4520  vfinncvntnn  4548  fun  5236  tz6.12c  5347  eqfnfv  5392  fnressn  5438  fressnfv  5439  fconst2g  5452  eloprabga  5578  ndmovcl  5614  fvmptnf  5723  mapsn  6026  mapss  6027  enprmaplem3  6078  sbthlem2  6204  nmembers1lem3  6270  nchoicelem12  6300