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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used 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  3701  ssuni  3957  disjiun  4125  trintssm  4245  ssexg  4272  pofun  4457  sowlin  4465  2optocl  4852  3optocl  4853  ssrelrn  4972  elrnmpt1  5033  resieq  5073  fnun  5489  fss  5546  fun  5561  dmfex  5582  fvelimab  5759  mptfvex  5791  fmptco  5874  fnressn  5901  fressnfv  5902  fvtp2g  5924  fvtp3g  5925  fnex  5937  funfvima3  5952  isores3  6021  f1o2ndf1  6464  funsssuppss  6498  reldmtpos  6524  smores  6563  tfrlem7  6588  tfrlemi1  6603  tfrexlem  6605  tfrcl  6635  frecrdg  6679  nnacl  6753  nnmcl  6754  nnmsucr  6761  nntri3or  6766  nnaword  6784  nnaordex  6801  2ecoptocl  6897  ssct  7114  enm  7118  xpf1o  7144  ac6sfi  7202  f1dmvrnfibi  7258  f1vrnfibi  7259  suppeqfsuppbi  7295  updjud  7422  enumct  7455  nnnninfeq  7468  exmidontriimlem4  7580  exmidontriim  7581  elni2  7681  ax1rid  8244  negf1o  8710  mulgt1  9195  lbreu  9277  nnaddcl  9326  nnmulcl  9327  zaddcllempos  9685  zaddcllemneg  9687  nn0n0n1ge2b  9729  fzind  9765  fnn0ind  9766  uzaddcl  9995  elpq  10059  uzsubsubfz  10462  elfz1b  10507  elfz0ubfz0  10542  fz0fzdiffz0  10547  elfzmlbp  10549  fzofzim  10610  elfzom1elp1fzo  10630  elfzom1p1elfzo  10642  ssfzo12bi  10653  modfzo0difsn  10845  seq3val  10910  seqvalcd  10911  expcllem  11000  expap0  11019  apexp1  11170  faclbnd  11193  faclbnd6  11196  fihashf1rn  11241  omgadd  11256  hashfzp1  11279  hashmap  11282  seq3coll  11308  fundm2domnop0  11314  lswlgt0cl  11371  ccatsymb  11384  swrdnd  11445  swrd0g  11446  swrdspsleq  11453  pfxsuff1eqwrdeq  11485  swrdswrdlem  11490  swrdswrd  11491  wrd2ind  11509  pfxccatin12lem2a  11513  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  cjexp  11672  r19.29uz  11772  resqrexlemover  11790  resqrexlemlo  11793  resqrexlemcalc3  11796  absexp  11860  fimaxre2  12008  climshft  12086  climub  12126  climserle  12127  sumfct  12156  isumss2  12176  binom  12267  bcxmas  12272  clim2prod  12322  prodfap0  12328  prodfrecap  12329  prodfct  12370  demoivreALT  12557  dvdsdivcl  12633  dvdsfac  12643  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  m1exp1  12684  nn0o  12690  flodddiv4  12719  gcdneg  12775  bezoutlemmain  12791  dfgcd2  12807  gcdmultiple  12813  nnwosdc  12832  alginv  12841  cncongr1  12897  prmdvdsexp  12943  prmndvdsfaclt  12951  dfgrp2  13881  srgmulgass  14342  lmodvsmmulgdi  14709  lmodfopnelem1  14710  rmodislmodlem  14736  cnfldmulg  14962  cnfldexp  14963  assamulgscm  15092  clsss  15268  xmettri2  15511  mettri  15523  metss  15644  plycolemc  15908  zabsle1  16216  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  2lgslem1a1  16303  incistruhgr  16429  umgrislfupgrenlem  16469  uhgr2edg  16545  usgredg2vlem2  16562  subgrfun  16606  wlkl1loop  16697  wlkres  16718  clwwlkccatlem  16739  isclwwlknx  16755  clwwlkext2edg  16761  clwwlknonel  16771  clwwlknonex2lem2  16777  clwwlknun  16780  depindlem2  16846  depindlem3  16847  bdssexg  17028  bj-findis  17103  nninfalllem1  17149  nninfsellemdc  17151  redc0  17205