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  1685  19.41  1686  equtr2  1711  mopick  2104  2euex  2113  gencl  2769  2gencl  2770  rspccva  2840  indifdir  3391  sseq0  3464  minel  3484  r19.2m  3509  r19.2mOLD  3510  elelpwi  3587  ssuni  3831  disjiun  3998  trintssm  4117  ssexg  4142  pofun  4312  sowlin  4320  2optocl  4703  3optocl  4704  elrnmpt1  4878  resieq  4917  fnun  5322  fss  5377  fun  5388  dmfex  5405  fvelimab  5572  mptfvex  5601  fmptco  5682  fnressn  5702  fressnfv  5703  fvtp2g  5725  fvtp3g  5726  fnex  5738  funfvima3  5750  isores3  5815  f1o2ndf1  6228  reldmtpos  6253  smores  6292  tfrlem7  6317  tfrlemi1  6332  tfrexlem  6334  tfrcl  6364  frecrdg  6408  nnacl  6480  nnmcl  6481  nnmsucr  6488  nntri3or  6493  nnaword  6511  nnaordex  6528  2ecoptocl  6622  ssct  6817  enm  6819  xpf1o  6843  ac6sfi  6897  f1dmvrnfibi  6942  f1vrnfibi  6943  updjud  7080  enumct  7113  nnnninfeq  7125  exmidontriimlem4  7222  exmidontriim  7223  elni2  7312  ax1rid  7875  negf1o  8338  mulgt1  8819  lbreu  8901  nnaddcl  8938  nnmulcl  8939  zaddcllempos  9289  zaddcllemneg  9291  nn0n0n1ge2b  9331  fzind  9367  fnn0ind  9368  uzaddcl  9585  elpq  9647  uzsubsubfz  10046  elfz1b  10089  elfz0ubfz0  10124  fz0fzdiffz0  10129  elfzmlbp  10131  fzofzim  10187  elfzom1elp1fzo  10201  elfzom1p1elfzo  10213  ssfzo12bi  10224  modfzo0difsn  10394  seq3val  10457  seqvalcd  10458  expcllem  10530  expap0  10549  apexp1  10697  faclbnd  10720  faclbnd6  10723  fihashf1rn  10767  omgadd  10781  hashfzp1  10803  seq3coll  10821  cjexp  10901  r19.29uz  11000  resqrexlemover  11018  resqrexlemlo  11021  resqrexlemcalc3  11024  absexp  11087  fimaxre2  11234  climshft  11311  climub  11351  climserle  11352  sumfct  11381  isumss2  11400  binom  11491  bcxmas  11496  clim2prod  11546  prodfap0  11552  prodfrecap  11553  prodfct  11594  demoivreALT  11780  dvdsdivcl  11855  dvdsfac  11865  oddnn02np1  11884  oddge22np1  11885  evennn02n  11886  evennn2n  11887  m1exp1  11905  nn0o  11911  flodddiv4  11938  gcdneg  11982  bezoutlemmain  11998  dfgcd2  12014  gcdmultiple  12020  nnwosdc  12039  alginv  12046  cncongr1  12102  prmdvdsexp  12147  prmndvdsfaclt  12155  dfgrp2  12901  srgmulgass  13170  cnfldmulg  13440  cnfldexp  13441  clsss  13588  xmettri2  13831  mettri  13843  metss  13964  zabsle1  14370  bdssexg  14626  bj-findis  14701  nninfalllem1  14727  nninfsellemdc  14729  redc0  14775