Theorem impcom 125

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 30	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 124	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  mpan9  281  19.41h  1695  19.41  1696  equtr2  1721  mopick  2115  2euex  2124  gencl  2783  2gencl  2784  rspccva  2854  indifdir  3405  sseq0  3478  minel  3498  r19.2m  3523  r19.2mOLD  3524  elelpwi  3601  ssuni  3845  disjiun  4012  trintssm  4131  ssexg  4156  pofun  4326  sowlin  4334  2optocl  4717  3optocl  4718  elrnmpt1  4892  resieq  4931  fnun  5336  fss  5391  fun  5402  dmfex  5419  fvelimab  5587  mptfvex  5616  fmptco  5697  fnressn  5717  fressnfv  5718  fvtp2g  5740  fvtp3g  5741  fnex  5753  funfvima3  5765  isores3  5831  f1o2ndf1  6246  reldmtpos  6271  smores  6310  tfrlem7  6335  tfrlemi1  6350  tfrexlem  6352  tfrcl  6382  frecrdg  6426  nnacl  6498  nnmcl  6499  nnmsucr  6506  nntri3or  6511  nnaword  6529  nnaordex  6546  2ecoptocl  6640  ssct  6835  enm  6837  xpf1o  6861  ac6sfi  6915  f1dmvrnfibi  6960  f1vrnfibi  6961  updjud  7098  enumct  7131  nnnninfeq  7143  exmidontriimlem4  7240  exmidontriim  7241  elni2  7330  ax1rid  7893  negf1o  8356  mulgt1  8837  lbreu  8919  nnaddcl  8956  nnmulcl  8957  zaddcllempos  9307  zaddcllemneg  9309  nn0n0n1ge2b  9349  fzind  9385  fnn0ind  9386  uzaddcl  9603  elpq  9665  uzsubsubfz  10064  elfz1b  10107  elfz0ubfz0  10142  fz0fzdiffz0  10147  elfzmlbp  10149  fzofzim  10205  elfzom1elp1fzo  10219  elfzom1p1elfzo  10231  ssfzo12bi  10242  modfzo0difsn  10412  seq3val  10475  seqvalcd  10476  expcllem  10548  expap0  10567  apexp1  10715  faclbnd  10738  faclbnd6  10741  fihashf1rn  10785  omgadd  10799  hashfzp1  10821  seq3coll  10839  cjexp  10919  r19.29uz  11018  resqrexlemover  11036  resqrexlemlo  11039  resqrexlemcalc3  11042  absexp  11105  fimaxre2  11252  climshft  11329  climub  11369  climserle  11370  sumfct  11399  isumss2  11418  binom  11509  bcxmas  11514  clim2prod  11564  prodfap0  11570  prodfrecap  11571  prodfct  11612  demoivreALT  11798  dvdsdivcl  11873  dvdsfac  11883  oddnn02np1  11902  oddge22np1  11903  evennn02n  11904  evennn2n  11905  m1exp1  11923  nn0o  11929  flodddiv4  11956  gcdneg  12000  bezoutlemmain  12016  dfgcd2  12032  gcdmultiple  12038  nnwosdc  12057  alginv  12064  cncongr1  12120  prmdvdsexp  12165  prmndvdsfaclt  12173  dfgrp2  12936  srgmulgass  13303  lmodvsmmulgdi  13599  lmodfopnelem1  13600  rmodislmodlem  13626  cnfldmulg  13839  cnfldexp  13840  clsss  14001  xmettri2  14244  mettri  14256  metss  14377  zabsle1  14783  bdssexg  15039  bj-findis  15114  nninfalllem1  15141  nninfsellemdc  15143  redc0  15189