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  1731  19.41  1732  equtr2  1757  mopick  2156  2euex  2165  gencl  2832  2gencl  2833  vtocl4g  2872  vtocl4ga  2873  rspccva  2906  indifdir  3460  sseq0  3533  minel  3553  r19.2m  3578  r19.2mOLD  3579  elelpwi  3661  ssuni  3910  disjiun  4078  trintssm  4198  ssexg  4223  pofun  4403  sowlin  4411  2optocl  4796  3optocl  4797  ssrelrn  4914  elrnmpt1  4975  resieq  5015  fnun  5429  fss  5485  fun  5499  dmfex  5517  fvelimab  5692  mptfvex  5722  fmptco  5803  fnressn  5829  fressnfv  5830  fvtp2g  5852  fvtp3g  5853  fnex  5865  funfvima3  5877  isores3  5945  f1o2ndf1  6380  reldmtpos  6405  smores  6444  tfrlem7  6469  tfrlemi1  6484  tfrexlem  6486  tfrcl  6516  frecrdg  6560  nnacl  6634  nnmcl  6635  nnmsucr  6642  nntri3or  6647  nnaword  6665  nnaordex  6682  2ecoptocl  6778  ssct  6983  enm  6987  xpf1o  7013  ac6sfi  7068  f1dmvrnfibi  7122  f1vrnfibi  7123  updjud  7260  enumct  7293  nnnninfeq  7306  exmidontriimlem4  7417  exmidontriim  7418  elni2  7512  ax1rid  8075  negf1o  8539  mulgt1  9021  lbreu  9103  nnaddcl  9141  nnmulcl  9142  zaddcllempos  9494  zaddcllemneg  9496  nn0n0n1ge2b  9537  fzind  9573  fnn0ind  9574  uzaddcl  9793  elpq  9856  uzsubsubfz  10255  elfz1b  10298  elfz0ubfz0  10333  fz0fzdiffz0  10338  elfzmlbp  10340  fzofzim  10400  elfzom1elp1fzo  10420  elfzom1p1elfzo  10432  ssfzo12bi  10443  modfzo0difsn  10629  seq3val  10694  seqvalcd  10695  expcllem  10784  expap0  10803  apexp1  10952  faclbnd  10975  faclbnd6  10978  fihashf1rn  11022  omgadd  11036  hashfzp1  11059  seq3coll  11077  fundm2domnop0  11080  lswlgt0cl  11137  ccatsymb  11150  swrdnd  11206  swrd0g  11207  swrdspsleq  11214  pfxsuff1eqwrdeq  11246  swrdswrdlem  11251  swrdswrd  11252  wrd2ind  11270  pfxccatin12lem2a  11274  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  pfxccat3a  11285  swrdccat3blem  11286  cjexp  11419  r19.29uz  11518  resqrexlemover  11536  resqrexlemlo  11539  resqrexlemcalc3  11542  absexp  11605  fimaxre2  11753  climshft  11830  climub  11870  climserle  11871  sumfct  11900  isumss2  11919  binom  12010  bcxmas  12015  clim2prod  12065  prodfap0  12071  prodfrecap  12072  prodfct  12113  demoivreALT  12300  dvdsdivcl  12376  dvdsfac  12386  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  m1exp1  12427  nn0o  12433  flodddiv4  12462  gcdneg  12518  bezoutlemmain  12534  dfgcd2  12550  gcdmultiple  12556  nnwosdc  12575  alginv  12584  cncongr1  12640  prmdvdsexp  12685  prmndvdsfaclt  12693  dfgrp2  13575  srgmulgass  13967  lmodvsmmulgdi  14302  lmodfopnelem1  14303  rmodislmodlem  14329  cnfldmulg  14555  cnfldexp  14556  clsss  14807  xmettri2  15050  mettri  15062  metss  15183  plycolemc  15447  zabsle1  15693  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  2lgslem1a1  15780  incistruhgr  15905  umgrislfupgrenlem  15943  uhgr2edg  16019  usgredg2vlem2  16036  wlkl1loop  16099  wlkres  16118  clwwlkccatlem  16137  bdssexg  16322  bj-findis  16397  nninfalllem1  16434  nninfsellemdc  16436  redc0  16485