Theorem expcom 424

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

Hypothesis

Ref	Expression
exp.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
expcom	|- (ps -> (ph -> ch))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	ex 423	. 2 |- (ph -> (ps -> ch))
3	2	com12 27	1 |- (ps -> (ph -> ch))

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:  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  2592  r19.21be  2716  uneqdifeq  3639  ssunsn2  3866  ssuni  3914  uniss2  3923  elpwuni  4054  lenltfin  4470  tfincl  4493  tfinltfin  4502  evenoddnnnul  4515  nnadjoin  4521  vfinncvntnn  4549  fun  5237  tz6.12c  5348  eqfnfv  5393  fnressn  5439  fressnfv  5440  fconst2g  5453  eloprabga  5579  ndmovcl  5615  fvmptnf  5724  mapsn  6027  mapss  6028  enprmaplem3  6079  sbthlem2  6205  nmembers1lem3  6271  nchoicelem12  6301