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  1737  19.41  1738  equtr2  1763  mopick  2165  2euex  2174  gencl  2854  2gencl  2855  vtocl4g  2894  vtocl4ga  2895  rspccva  2928  indifdir  3487  minel  3586  r19.2m  3614  r19.2mOLD  3615  elelpwi  3700  ssuni  3955  disjiun  4123  trintssm  4243  ssexg  4270  pofun  4455  sowlin  4463  2optocl  4850  3optocl  4851  ssrelrn  4970  elrnmpt1  5031  resieq  5071  fnun  5487  fss  5544  fun  5559  dmfex  5580  fvelimab  5756  mptfvex  5788  fmptco  5868  fnressn  5895  fressnfv  5896  fvtp2g  5918  fvtp3g  5919  fnex  5931  funfvima3  5945  isores3  6014  f1o2ndf1  6457  funsssuppss  6491  reldmtpos  6517  smores  6556  tfrlem7  6581  tfrlemi1  6596  tfrexlem  6598  tfrcl  6628  frecrdg  6672  nnacl  6746  nnmcl  6747  nnmsucr  6754  nntri3or  6759  nnaword  6777  nnaordex  6794  2ecoptocl  6890  ssct  7107  enm  7111  xpf1o  7137  ac6sfi  7195  f1dmvrnfibi  7251  f1vrnfibi  7252  suppeqfsuppbi  7288  updjud  7415  enumct  7448  nnnninfeq  7461  exmidontriimlem4  7573  exmidontriim  7574  elni2  7674  ax1rid  8237  negf1o  8702  mulgt1  9186  lbreu  9268  nnaddcl  9306  nnmulcl  9307  zaddcllempos  9663  zaddcllemneg  9665  nn0n0n1ge2b  9707  fzind  9743  fnn0ind  9744  uzaddcl  9968  elpq  10031  uzsubsubfz  10433  elfz1b  10478  elfz0ubfz0  10513  fz0fzdiffz0  10518  elfzmlbp  10520  fzofzim  10581  elfzom1elp1fzo  10601  elfzom1p1elfzo  10613  ssfzo12bi  10624  modfzo0difsn  10813  seq3val  10878  seqvalcd  10879  expcllem  10968  expap0  10987  apexp1  11137  faclbnd  11160  faclbnd6  11163  fihashf1rn  11208  omgadd  11223  hashfzp1  11246  hashmap  11249  seq3coll  11275  fundm2domnop0  11281  lswlgt0cl  11338  ccatsymb  11351  swrdnd  11412  swrd0g  11413  swrdspsleq  11420  pfxsuff1eqwrdeq  11452  swrdswrdlem  11457  swrdswrd  11458  wrd2ind  11476  pfxccatin12lem2a  11480  swrdccatin2  11482  pfxccatin12lem2  11484  pfxccatin12lem3  11485  pfxccatin12  11486  pfxccat3  11487  swrdccat  11488  pfxccat3a  11491  swrdccat3blem  11492  cjexp  11639  r19.29uz  11739  resqrexlemover  11757  resqrexlemlo  11760  resqrexlemcalc3  11763  absexp  11826  fimaxre2  11974  climshft  12051  climub  12091  climserle  12092  sumfct  12121  isumss2  12141  binom  12232  bcxmas  12237  clim2prod  12287  prodfap0  12293  prodfrecap  12294  prodfct  12335  demoivreALT  12522  dvdsdivcl  12598  dvdsfac  12608  oddnn02np1  12628  oddge22np1  12629  evennn02n  12630  evennn2n  12631  m1exp1  12649  nn0o  12655  flodddiv4  12684  gcdneg  12740  bezoutlemmain  12756  dfgcd2  12772  gcdmultiple  12778  nnwosdc  12797  alginv  12806  cncongr1  12862  prmdvdsexp  12907  prmndvdsfaclt  12915  dfgrp2  13812  srgmulgass  14270  lmodvsmmulgdi  14635  lmodfopnelem1  14636  rmodislmodlem  14662  cnfldmulg  14888  cnfldexp  14889  clsss  15145  xmettri2  15388  mettri  15400  metss  15521  plycolemc  15785  zabsle1  16035  gausslemma2dlem1a  16094  gausslemma2dlem2  16098  gausslemma2dlem3  16099  gausslemma2dlem4  16100  2lgslem1a1  16122  incistruhgr  16248  umgrislfupgrenlem  16288  uhgr2edg  16364  usgredg2vlem2  16381  subgrfun  16425  wlkl1loop  16516  wlkres  16537  clwwlkccatlem  16558  isclwwlknx  16574  clwwlkext2edg  16580  clwwlknonel  16590  clwwlknonex2lem2  16596  clwwlknun  16599  depindlem2  16665  depindlem3  16666  bdssexg  16847  bj-findis  16922  nninfalllem1  16959  nninfsellemdc  16961  redc0  17015