Theorem impcom 125

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
impcom	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

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  1699  19.41  1700  equtr2  1725  mopick  2123  2euex  2132  gencl  2795  2gencl  2796  rspccva  2867  indifdir  3420  sseq0  3493  minel  3513  r19.2m  3538  r19.2mOLD  3539  elelpwi  3618  ssuni  3862  disjiun  4029  trintssm  4148  ssexg  4173  pofun  4348  sowlin  4356  2optocl  4741  3optocl  4742  elrnmpt1  4918  resieq  4957  fnun  5367  fss  5422  fun  5433  dmfex  5450  fvelimab  5620  mptfvex  5650  fmptco  5731  fnressn  5751  fressnfv  5752  fvtp2g  5774  fvtp3g  5775  fnex  5787  funfvima3  5799  isores3  5865  f1o2ndf1  6295  reldmtpos  6320  smores  6359  tfrlem7  6384  tfrlemi1  6399  tfrexlem  6401  tfrcl  6431  frecrdg  6475  nnacl  6547  nnmcl  6548  nnmsucr  6555  nntri3or  6560  nnaword  6578  nnaordex  6595  2ecoptocl  6691  ssct  6886  enm  6888  xpf1o  6914  ac6sfi  6968  f1dmvrnfibi  7019  f1vrnfibi  7020  updjud  7157  enumct  7190  nnnninfeq  7203  exmidontriimlem4  7307  exmidontriim  7308  elni2  7398  ax1rid  7961  negf1o  8425  mulgt1  8907  lbreu  8989  nnaddcl  9027  nnmulcl  9028  zaddcllempos  9380  zaddcllemneg  9382  nn0n0n1ge2b  9422  fzind  9458  fnn0ind  9459  uzaddcl  9677  elpq  9740  uzsubsubfz  10139  elfz1b  10182  elfz0ubfz0  10217  fz0fzdiffz0  10222  elfzmlbp  10224  fzofzim  10281  elfzom1elp1fzo  10295  elfzom1p1elfzo  10307  ssfzo12bi  10318  modfzo0difsn  10504  seq3val  10569  seqvalcd  10570  expcllem  10659  expap0  10678  apexp1  10827  faclbnd  10850  faclbnd6  10853  fihashf1rn  10897  omgadd  10911  hashfzp1  10933  seq3coll  10951  cjexp  11075  r19.29uz  11174  resqrexlemover  11192  resqrexlemlo  11195  resqrexlemcalc3  11198  absexp  11261  fimaxre2  11409  climshft  11486  climub  11526  climserle  11527  sumfct  11556  isumss2  11575  binom  11666  bcxmas  11671  clim2prod  11721  prodfap0  11727  prodfrecap  11728  prodfct  11769  demoivreALT  11956  dvdsdivcl  12032  dvdsfac  12042  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  m1exp1  12083  nn0o  12089  flodddiv4  12118  gcdneg  12174  bezoutlemmain  12190  dfgcd2  12206  gcdmultiple  12212  nnwosdc  12231  alginv  12240  cncongr1  12296  prmdvdsexp  12341  prmndvdsfaclt  12349  dfgrp2  13229  srgmulgass  13621  lmodvsmmulgdi  13955  lmodfopnelem1  13956  rmodislmodlem  13982  cnfldmulg  14208  cnfldexp  14209  clsss  14438  xmettri2  14681  mettri  14693  metss  14814  plycolemc  15078  zabsle1  15324  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  2lgslem1a1  15411  bdssexg  15634  bj-findis  15709  nninfalllem1  15739  nninfsellemdc  15741  redc0  15788