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  2835  2gencl  2836  vtocl4g  2875  vtocl4ga  2876  rspccva  2909  indifdir  3463  sseq0  3536  minel  3556  r19.2m  3581  r19.2mOLD  3582  elelpwi  3664  ssuni  3915  disjiun  4083  trintssm  4203  ssexg  4228  pofun  4409  sowlin  4417  2optocl  4803  3optocl  4804  ssrelrn  4922  elrnmpt1  4983  resieq  5023  fnun  5438  fss  5494  fun  5508  dmfex  5526  fvelimab  5702  mptfvex  5732  fmptco  5813  fnressn  5840  fressnfv  5841  fvtp2g  5863  fvtp3g  5864  fnex  5876  funfvima3  5888  isores3  5956  f1o2ndf1  6393  reldmtpos  6419  smores  6458  tfrlem7  6483  tfrlemi1  6498  tfrexlem  6500  tfrcl  6530  frecrdg  6574  nnacl  6648  nnmcl  6649  nnmsucr  6656  nntri3or  6661  nnaword  6679  nnaordex  6696  2ecoptocl  6792  ssct  7000  enm  7004  xpf1o  7030  ac6sfi  7087  f1dmvrnfibi  7143  f1vrnfibi  7144  updjud  7281  enumct  7314  nnnninfeq  7327  exmidontriimlem4  7439  exmidontriim  7440  elni2  7534  ax1rid  8097  negf1o  8561  mulgt1  9043  lbreu  9125  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  nn0n0n1ge2b  9559  fzind  9595  fnn0ind  9596  uzaddcl  9820  elpq  9883  uzsubsubfz  10282  elfz1b  10325  elfz0ubfz0  10360  fz0fzdiffz0  10365  elfzmlbp  10367  fzofzim  10428  elfzom1elp1fzo  10448  elfzom1p1elfzo  10460  ssfzo12bi  10471  modfzo0difsn  10658  seq3val  10723  seqvalcd  10724  expcllem  10813  expap0  10832  apexp1  10981  faclbnd  11004  faclbnd6  11007  fihashf1rn  11051  omgadd  11066  hashfzp1  11089  seq3coll  11107  fundm2domnop0  11113  lswlgt0cl  11170  ccatsymb  11183  swrdnd  11244  swrd0g  11245  swrdspsleq  11252  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  swrdswrd  11290  wrd2ind  11308  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  cjexp  11471  r19.29uz  11570  resqrexlemover  11588  resqrexlemlo  11591  resqrexlemcalc3  11594  absexp  11657  fimaxre2  11805  climshft  11882  climub  11922  climserle  11923  sumfct  11952  isumss2  11972  binom  12063  bcxmas  12068  clim2prod  12118  prodfap0  12124  prodfrecap  12125  prodfct  12166  demoivreALT  12353  dvdsdivcl  12429  dvdsfac  12439  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  m1exp1  12480  nn0o  12486  flodddiv4  12515  gcdneg  12571  bezoutlemmain  12587  dfgcd2  12603  gcdmultiple  12609  nnwosdc  12628  alginv  12637  cncongr1  12693  prmdvdsexp  12738  prmndvdsfaclt  12746  dfgrp2  13628  srgmulgass  14021  lmodvsmmulgdi  14356  lmodfopnelem1  14357  rmodislmodlem  14383  cnfldmulg  14609  cnfldexp  14610  clsss  14861  xmettri2  15104  mettri  15116  metss  15237  plycolemc  15501  zabsle1  15747  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  2lgslem1a1  15834  incistruhgr  15960  umgrislfupgrenlem  16000  uhgr2edg  16076  usgredg2vlem2  16093  subgrfun  16137  wlkl1loop  16228  wlkres  16249  clwwlkccatlem  16270  isclwwlknx  16286  clwwlkext2edg  16292  clwwlknonel  16302  clwwlknonex2lem2  16308  clwwlknun  16311  depindlem2  16377  depindlem3  16378  bdssexg  16550  bj-findis  16625  nninfalllem1  16661  nninfsellemdc  16663  redc0  16713