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  1731  19.41  1732  equtr2  1757  mopick  2156  2euex  2165  gencl  2832  2gencl  2833  vtocl4g  2872  vtocl4ga  2873  rspccva  2906  indifdir  3460  sseq0  3533  minel  3553  r19.2m  3578  r19.2mOLD  3579  elelpwi  3661  ssuni  3910  disjiun  4078  trintssm  4198  ssexg  4223  pofun  4403  sowlin  4411  2optocl  4796  3optocl  4797  ssrelrn  4914  elrnmpt1  4975  resieq  5015  fnun  5429  fss  5485  fun  5499  dmfex  5517  fvelimab  5692  mptfvex  5722  fmptco  5803  fnressn  5829  fressnfv  5830  fvtp2g  5852  fvtp3g  5853  fnex  5865  funfvima3  5877  isores3  5945  f1o2ndf1  6380  reldmtpos  6405  smores  6444  tfrlem7  6469  tfrlemi1  6484  tfrexlem  6486  tfrcl  6516  frecrdg  6560  nnacl  6634  nnmcl  6635  nnmsucr  6642  nntri3or  6647  nnaword  6665  nnaordex  6682  2ecoptocl  6778  ssct  6983  enm  6987  xpf1o  7013  ac6sfi  7068  f1dmvrnfibi  7122  f1vrnfibi  7123  updjud  7260  enumct  7293  nnnninfeq  7306  exmidontriimlem4  7417  exmidontriim  7418  elni2  7512  ax1rid  8075  negf1o  8539  mulgt1  9021  lbreu  9103  nnaddcl  9141  nnmulcl  9142  zaddcllempos  9494  zaddcllemneg  9496  nn0n0n1ge2b  9537  fzind  9573  fnn0ind  9574  uzaddcl  9793  elpq  9856  uzsubsubfz  10255  elfz1b  10298  elfz0ubfz0  10333  fz0fzdiffz0  10338  elfzmlbp  10340  fzofzim  10400  elfzom1elp1fzo  10420  elfzom1p1elfzo  10432  ssfzo12bi  10443  modfzo0difsn  10629  seq3val  10694  seqvalcd  10695  expcllem  10784  expap0  10803  apexp1  10952  faclbnd  10975  faclbnd6  10978  fihashf1rn  11022  omgadd  11036  hashfzp1  11059  seq3coll  11077  fundm2domnop0  11080  lswlgt0cl  11137  ccatsymb  11150  swrdnd  11207  swrd0g  11208  swrdspsleq  11215  pfxsuff1eqwrdeq  11247  swrdswrdlem  11252  swrdswrd  11253  wrd2ind  11271  pfxccatin12lem2a  11275  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  pfxccat3a  11286  swrdccat3blem  11287  cjexp  11420  r19.29uz  11519  resqrexlemover  11537  resqrexlemlo  11540  resqrexlemcalc3  11543  absexp  11606  fimaxre2  11754  climshft  11831  climub  11871  climserle  11872  sumfct  11901  isumss2  11920  binom  12011  bcxmas  12016  clim2prod  12066  prodfap0  12072  prodfrecap  12073  prodfct  12114  demoivreALT  12301  dvdsdivcl  12377  dvdsfac  12387  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  m1exp1  12428  nn0o  12434  flodddiv4  12463  gcdneg  12519  bezoutlemmain  12535  dfgcd2  12551  gcdmultiple  12557  nnwosdc  12576  alginv  12585  cncongr1  12641  prmdvdsexp  12686  prmndvdsfaclt  12694  dfgrp2  13576  srgmulgass  13968  lmodvsmmulgdi  14303  lmodfopnelem1  14304  rmodislmodlem  14330  cnfldmulg  14556  cnfldexp  14557  clsss  14808  xmettri2  15051  mettri  15063  metss  15184  plycolemc  15448  zabsle1  15694  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem3  15758  gausslemma2dlem4  15759  2lgslem1a1  15781  incistruhgr  15906  umgrislfupgrenlem  15944  uhgr2edg  16020  usgredg2vlem2  16037  wlkl1loop  16104  wlkres  16123  clwwlkccatlem  16143  isclwwlknx  16158  clwwlkext2edg  16164  bdssexg  16350  bj-findis  16425  nninfalllem1  16462  nninfsellemdc  16464  redc0  16513