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  1696  19.41  1697  equtr2  1722  mopick  2120  2euex  2129  gencl  2792  2gencl  2793  rspccva  2864  indifdir  3416  sseq0  3489  minel  3509  r19.2m  3534  r19.2mOLD  3535  elelpwi  3614  ssuni  3858  disjiun  4025  trintssm  4144  ssexg  4169  pofun  4344  sowlin  4352  2optocl  4737  3optocl  4738  elrnmpt1  4914  resieq  4953  fnun  5361  fss  5416  fun  5427  dmfex  5444  fvelimab  5614  mptfvex  5644  fmptco  5725  fnressn  5745  fressnfv  5746  fvtp2g  5768  fvtp3g  5769  fnex  5781  funfvima3  5793  isores3  5859  f1o2ndf1  6283  reldmtpos  6308  smores  6347  tfrlem7  6372  tfrlemi1  6387  tfrexlem  6389  tfrcl  6419  frecrdg  6463  nnacl  6535  nnmcl  6536  nnmsucr  6543  nntri3or  6548  nnaword  6566  nnaordex  6583  2ecoptocl  6679  ssct  6874  enm  6876  xpf1o  6902  ac6sfi  6956  f1dmvrnfibi  7005  f1vrnfibi  7006  updjud  7143  enumct  7176  nnnninfeq  7189  exmidontriimlem4  7286  exmidontriim  7287  elni2  7376  ax1rid  7939  negf1o  8403  mulgt1  8884  lbreu  8966  nnaddcl  9004  nnmulcl  9005  zaddcllempos  9357  zaddcllemneg  9359  nn0n0n1ge2b  9399  fzind  9435  fnn0ind  9436  uzaddcl  9654  elpq  9717  uzsubsubfz  10116  elfz1b  10159  elfz0ubfz0  10194  fz0fzdiffz0  10199  elfzmlbp  10201  fzofzim  10258  elfzom1elp1fzo  10272  elfzom1p1elfzo  10284  ssfzo12bi  10295  modfzo0difsn  10469  seq3val  10534  seqvalcd  10535  expcllem  10624  expap0  10643  apexp1  10792  faclbnd  10815  faclbnd6  10818  fihashf1rn  10862  omgadd  10876  hashfzp1  10898  seq3coll  10916  cjexp  11040  r19.29uz  11139  resqrexlemover  11157  resqrexlemlo  11160  resqrexlemcalc3  11163  absexp  11226  fimaxre2  11373  climshft  11450  climub  11490  climserle  11491  sumfct  11520  isumss2  11539  binom  11630  bcxmas  11635  clim2prod  11685  prodfap0  11691  prodfrecap  11692  prodfct  11733  demoivreALT  11920  dvdsdivcl  11995  dvdsfac  12005  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  m1exp1  12045  nn0o  12051  flodddiv4  12078  gcdneg  12122  bezoutlemmain  12138  dfgcd2  12154  gcdmultiple  12160  nnwosdc  12179  alginv  12188  cncongr1  12244  prmdvdsexp  12289  prmndvdsfaclt  12297  dfgrp2  13102  srgmulgass  13488  lmodvsmmulgdi  13822  lmodfopnelem1  13823  rmodislmodlem  13849  cnfldmulg  14075  cnfldexp  14076  clsss  14297  xmettri2  14540  mettri  14552  metss  14673  plycolemc  14936  zabsle1  15156  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  2lgslem1a1  15243  bdssexg  15466  bj-findis  15541  nninfalllem1  15568  nninfsellemdc  15570  redc0  15617