Theorem impcom 419

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

Hypothesis

Ref	Expression
imp.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
impcom	|- ((ps /\ ph) -> ch)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 |- (ph -> (ps -> ch))
2	1	com12 27	. 2 |- (ps -> (ph -> ch))
3	2	imp 418	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:  mpan9  455  equtr2  1688  19.41  1879  dvelimf  1997  ax11eq  2193  ax11el  2194  mopick  2266  2euex  2276  gencl  2887  2gencl  2888  rspccva  2954  sbcimdv  3107  sseq0  3582  minel  3606  r19.2z  3639  elelpwi  3732  ssuni  3913  unipw  4117  pwadjoin  4119  opkthg  4131  sspw1  4335  findsd  4410  nnsucelr  4428  nndisjeq  4429  tfin11  4493  spfinsfincl  4539  phi11lem1  4595  phialllem1  4616  2optocl  4839  3optocl  4840  fneu  5187  fnun  5189  fss  5230  fun  5236  dmfex  5247  fvelimab  5370  eqfnfv  5392  fnressn  5438  fressnfv  5439  funfvima3  5461  f1fveq  5473  isotr  5495  ndmovcl  5614  fvmptss  5705  fnfullfunlem2  5857  clos1conn  5879  clos1basesuc  5882  2ecoptocl  5997  ce0addcnnul  6179  sbthlem2  6204  nchoicelem12  6300  frecxp  6314