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  1708  19.41  1709  equtr2  1734  mopick  2132  2euex  2141  gencl  2804  2gencl  2805  rspccva  2876  indifdir  3429  sseq0  3502  minel  3522  r19.2m  3547  r19.2mOLD  3548  elelpwi  3628  ssuni  3872  disjiun  4040  trintssm  4159  ssexg  4184  pofun  4360  sowlin  4368  2optocl  4753  3optocl  4754  elrnmpt1  4930  resieq  4970  fnun  5383  fss  5439  fun  5450  dmfex  5467  fvelimab  5637  mptfvex  5667  fmptco  5748  fnressn  5772  fressnfv  5773  fvtp2g  5795  fvtp3g  5796  fnex  5808  funfvima3  5820  isores3  5886  f1o2ndf1  6316  reldmtpos  6341  smores  6380  tfrlem7  6405  tfrlemi1  6420  tfrexlem  6422  tfrcl  6452  frecrdg  6496  nnacl  6568  nnmcl  6569  nnmsucr  6576  nntri3or  6581  nnaword  6599  nnaordex  6616  2ecoptocl  6712  ssct  6915  enm  6917  xpf1o  6943  ac6sfi  6997  f1dmvrnfibi  7048  f1vrnfibi  7049  updjud  7186  enumct  7219  nnnninfeq  7232  exmidontriimlem4  7338  exmidontriim  7339  elni2  7429  ax1rid  7992  negf1o  8456  mulgt1  8938  lbreu  9020  nnaddcl  9058  nnmulcl  9059  zaddcllempos  9411  zaddcllemneg  9413  nn0n0n1ge2b  9454  fzind  9490  fnn0ind  9491  uzaddcl  9709  elpq  9772  uzsubsubfz  10171  elfz1b  10214  elfz0ubfz0  10249  fz0fzdiffz0  10254  elfzmlbp  10256  fzofzim  10314  elfzom1elp1fzo  10333  elfzom1p1elfzo  10345  ssfzo12bi  10356  modfzo0difsn  10542  seq3val  10607  seqvalcd  10608  expcllem  10697  expap0  10716  apexp1  10865  faclbnd  10888  faclbnd6  10891  fihashf1rn  10935  omgadd  10949  hashfzp1  10971  seq3coll  10989  fundm2domnop0  10992  lswlgt0cl  11048  ccatsymb  11061  swrdnd  11115  swrd0g  11116  swrdspsleq  11123  pfxsuff1eqwrdeq  11153  cjexp  11237  r19.29uz  11336  resqrexlemover  11354  resqrexlemlo  11357  resqrexlemcalc3  11360  absexp  11423  fimaxre2  11571  climshft  11648  climub  11688  climserle  11689  sumfct  11718  isumss2  11737  binom  11828  bcxmas  11833  clim2prod  11883  prodfap0  11889  prodfrecap  11890  prodfct  11931  demoivreALT  12118  dvdsdivcl  12194  dvdsfac  12204  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  m1exp1  12245  nn0o  12251  flodddiv4  12280  gcdneg  12336  bezoutlemmain  12352  dfgcd2  12368  gcdmultiple  12374  nnwosdc  12393  alginv  12402  cncongr1  12458  prmdvdsexp  12503  prmndvdsfaclt  12511  dfgrp2  13392  srgmulgass  13784  lmodvsmmulgdi  14118  lmodfopnelem1  14119  rmodislmodlem  14145  cnfldmulg  14371  cnfldexp  14372  clsss  14623  xmettri2  14866  mettri  14878  metss  14999  plycolemc  15263  zabsle1  15509  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem3  15573  gausslemma2dlem4  15574  2lgslem1a1  15596  bdssexg  15877  bj-findis  15952  nninfalllem1  15982  nninfsellemdc  15984  redc0  16033