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  1733  19.41  1734  equtr2  1759  mopick  2158  2euex  2167  gencl  2835  2gencl  2836  vtocl4g  2875  vtocl4ga  2876  rspccva  2909  indifdir  3463  sseq0  3536  minel  3556  r19.2m  3581  r19.2mOLD  3582  elelpwi  3664  ssuni  3915  disjiun  4083  trintssm  4203  ssexg  4228  pofun  4409  sowlin  4417  2optocl  4803  3optocl  4804  ssrelrn  4922  elrnmpt1  4983  resieq  5023  fnun  5438  fss  5494  fun  5508  dmfex  5526  fvelimab  5702  mptfvex  5732  fmptco  5813  fnressn  5839  fressnfv  5840  fvtp2g  5862  fvtp3g  5863  fnex  5875  funfvima3  5887  isores3  5955  f1o2ndf1  6392  reldmtpos  6418  smores  6457  tfrlem7  6482  tfrlemi1  6497  tfrexlem  6499  tfrcl  6529  frecrdg  6573  nnacl  6647  nnmcl  6648  nnmsucr  6655  nntri3or  6660  nnaword  6678  nnaordex  6695  2ecoptocl  6791  ssct  6999  enm  7003  xpf1o  7029  ac6sfi  7086  f1dmvrnfibi  7142  f1vrnfibi  7143  updjud  7280  enumct  7313  nnnninfeq  7326  exmidontriimlem4  7438  exmidontriim  7439  elni2  7533  ax1rid  8096  negf1o  8560  mulgt1  9042  lbreu  9124  nnaddcl  9162  nnmulcl  9163  zaddcllempos  9515  zaddcllemneg  9517  nn0n0n1ge2b  9558  fzind  9594  fnn0ind  9595  uzaddcl  9819  elpq  9882  uzsubsubfz  10281  elfz1b  10324  elfz0ubfz0  10359  fz0fzdiffz0  10364  elfzmlbp  10366  fzofzim  10426  elfzom1elp1fzo  10446  elfzom1p1elfzo  10458  ssfzo12bi  10469  modfzo0difsn  10656  seq3val  10721  seqvalcd  10722  expcllem  10811  expap0  10830  apexp1  10979  faclbnd  11002  faclbnd6  11005  fihashf1rn  11049  omgadd  11064  hashfzp1  11087  seq3coll  11105  fundm2domnop0  11108  lswlgt0cl  11165  ccatsymb  11178  swrdnd  11239  swrd0g  11240  swrdspsleq  11247  pfxsuff1eqwrdeq  11279  swrdswrdlem  11284  swrdswrd  11285  wrd2ind  11303  pfxccatin12lem2a  11307  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  pfxccat3a  11318  swrdccat3blem  11319  cjexp  11453  r19.29uz  11552  resqrexlemover  11570  resqrexlemlo  11573  resqrexlemcalc3  11576  absexp  11639  fimaxre2  11787  climshft  11864  climub  11904  climserle  11905  sumfct  11934  isumss2  11953  binom  12044  bcxmas  12049  clim2prod  12099  prodfap0  12105  prodfrecap  12106  prodfct  12147  demoivreALT  12334  dvdsdivcl  12410  dvdsfac  12420  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  m1exp1  12461  nn0o  12467  flodddiv4  12496  gcdneg  12552  bezoutlemmain  12568  dfgcd2  12584  gcdmultiple  12590  nnwosdc  12609  alginv  12618  cncongr1  12674  prmdvdsexp  12719  prmndvdsfaclt  12727  dfgrp2  13609  srgmulgass  14001  lmodvsmmulgdi  14336  lmodfopnelem1  14337  rmodislmodlem  14363  cnfldmulg  14589  cnfldexp  14590  clsss  14841  xmettri2  15084  mettri  15096  metss  15217  plycolemc  15481  zabsle1  15727  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  2lgslem1a1  15814  incistruhgr  15940  umgrislfupgrenlem  15980  uhgr2edg  16056  usgredg2vlem2  16073  subgrfun  16117  wlkl1loop  16208  wlkres  16229  clwwlkccatlem  16250  isclwwlknx  16266  clwwlkext2edg  16272  clwwlknonel  16282  clwwlknonex2lem2  16288  clwwlknun  16291  bdssexg  16499  bj-findis  16574  nninfalllem1  16610  nninfsellemdc  16612  redc0  16661