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  1733  19.41  1734  equtr2  1759  mopick  2158  2euex  2167  gencl  2836  2gencl  2837  vtocl4g  2876  vtocl4ga  2877  rspccva  2910  indifdir  3465  sseq0  3538  minel  3558  r19.2m  3583  r19.2mOLD  3584  elelpwi  3668  ssuni  3920  disjiun  4088  trintssm  4208  ssexg  4233  pofun  4415  sowlin  4423  2optocl  4809  3optocl  4810  ssrelrn  4928  elrnmpt1  4989  resieq  5029  fnun  5445  fss  5501  fun  5516  dmfex  5535  fvelimab  5711  mptfvex  5741  fmptco  5821  fnressn  5848  fressnfv  5849  fvtp2g  5871  fvtp3g  5872  fnex  5884  funfvima3  5898  isores3  5966  f1o2ndf1  6402  funsssuppss  6436  reldmtpos  6462  smores  6501  tfrlem7  6526  tfrlemi1  6541  tfrexlem  6543  tfrcl  6573  frecrdg  6617  nnacl  6691  nnmcl  6692  nnmsucr  6699  nntri3or  6704  nnaword  6722  nnaordex  6739  2ecoptocl  6835  ssct  7043  enm  7047  xpf1o  7073  ac6sfi  7130  f1dmvrnfibi  7186  f1vrnfibi  7187  suppeqfsuppbi  7220  updjud  7341  enumct  7374  nnnninfeq  7387  exmidontriimlem4  7499  exmidontriim  7500  elni2  7594  ax1rid  8157  negf1o  8620  mulgt1  9102  lbreu  9184  nnaddcl  9222  nnmulcl  9223  zaddcllempos  9577  zaddcllemneg  9579  nn0n0n1ge2b  9620  fzind  9656  fnn0ind  9657  uzaddcl  9881  elpq  9944  uzsubsubfz  10344  elfz1b  10387  elfz0ubfz0  10422  fz0fzdiffz0  10427  elfzmlbp  10429  fzofzim  10490  elfzom1elp1fzo  10510  elfzom1p1elfzo  10522  ssfzo12bi  10533  modfzo0difsn  10720  seq3val  10785  seqvalcd  10786  expcllem  10875  expap0  10894  apexp1  11043  faclbnd  11066  faclbnd6  11069  fihashf1rn  11113  omgadd  11128  hashfzp1  11151  seq3coll  11169  fundm2domnop0  11175  lswlgt0cl  11232  ccatsymb  11245  swrdnd  11306  swrd0g  11307  swrdspsleq  11314  pfxsuff1eqwrdeq  11346  swrdswrdlem  11351  swrdswrd  11352  wrd2ind  11370  pfxccatin12lem2a  11374  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  pfxccat3a  11385  swrdccat3blem  11386  cjexp  11533  r19.29uz  11632  resqrexlemover  11650  resqrexlemlo  11653  resqrexlemcalc3  11656  absexp  11719  fimaxre2  11867  climshft  11944  climub  11984  climserle  11985  sumfct  12014  isumss2  12034  binom  12125  bcxmas  12130  clim2prod  12180  prodfap0  12186  prodfrecap  12187  prodfct  12228  demoivreALT  12415  dvdsdivcl  12491  dvdsfac  12501  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  m1exp1  12542  nn0o  12548  flodddiv4  12577  gcdneg  12633  bezoutlemmain  12649  dfgcd2  12665  gcdmultiple  12671  nnwosdc  12690  alginv  12699  cncongr1  12755  prmdvdsexp  12800  prmndvdsfaclt  12808  dfgrp2  13690  srgmulgass  14083  lmodvsmmulgdi  14419  lmodfopnelem1  14420  rmodislmodlem  14446  cnfldmulg  14672  cnfldexp  14673  clsss  14929  xmettri2  15172  mettri  15184  metss  15305  plycolemc  15569  zabsle1  15818  gausslemma2dlem1a  15877  gausslemma2dlem2  15881  gausslemma2dlem3  15882  gausslemma2dlem4  15883  2lgslem1a1  15905  incistruhgr  16031  umgrislfupgrenlem  16071  uhgr2edg  16147  usgredg2vlem2  16164  subgrfun  16208  wlkl1loop  16299  wlkres  16320  clwwlkccatlem  16341  isclwwlknx  16357  clwwlkext2edg  16363  clwwlknonel  16373  clwwlknonex2lem2  16379  clwwlknun  16382  depindlem2  16448  depindlem3  16449  bdssexg  16620  bj-findis  16695  nninfalllem1  16734  nninfsellemdc  16736  redc0  16790