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  2888  2gencl  2889  rspccva  2955  sbcimdv  3108  sseq0  3583  minel  3607  r19.2z  3640  elelpwi  3733  ssuni  3914  unipw  4118  pwadjoin  4120  opkthg  4132  sspw1  4336  findsd  4411  nnsucelr  4429  nndisjeq  4430  tfin11  4494  spfinsfincl  4540  phi11lem1  4596  phialllem1  4617  2optocl  4840  3optocl  4841  fneu  5188  fnun  5190  fss  5231  fun  5237  dmfex  5248  fvelimab  5371  eqfnfv  5393  fnressn  5439  fressnfv  5440  funfvima3  5462  f1fveq  5474  isotr  5496  ndmovcl  5615  fvmptss  5706  fnfullfunlem2  5858  clos1conn  5880  clos1basesuc  5883  2ecoptocl  5998  ce0addcnnul  6180  sbthlem2  6205  nchoicelem12  6301  frecxp  6315