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  2161  2euex  2170  gencl  2848  2gencl  2849  vtocl4g  2888  vtocl4ga  2889  rspccva  2922  indifdir  3481  sseq0  3554  minel  3574  r19.2m  3600  r19.2mOLD  3601  elelpwi  3686  ssuni  3941  disjiun  4109  trintssm  4229  ssexg  4254  pofun  4438  sowlin  4446  2optocl  4832  3optocl  4833  ssrelrn  4952  elrnmpt1  5013  resieq  5053  fnun  5469  fss  5526  fun  5541  dmfex  5562  fvelimab  5738  mptfvex  5768  fmptco  5848  fnressn  5875  fressnfv  5876  fvtp2g  5898  fvtp3g  5899  fnex  5911  funfvima3  5925  isores3  5994  f1o2ndf1  6437  funsssuppss  6471  reldmtpos  6497  smores  6536  tfrlem7  6561  tfrlemi1  6576  tfrexlem  6578  tfrcl  6608  frecrdg  6652  nnacl  6726  nnmcl  6727  nnmsucr  6734  nntri3or  6739  nnaword  6757  nnaordex  6774  2ecoptocl  6870  ssct  7080  enm  7084  xpf1o  7110  ac6sfi  7168  f1dmvrnfibi  7224  f1vrnfibi  7225  suppeqfsuppbi  7261  updjud  7386  enumct  7419  nnnninfeq  7432  exmidontriimlem4  7544  exmidontriim  7545  elni2  7645  ax1rid  8208  negf1o  8672  mulgt1  9154  lbreu  9236  nnaddcl  9274  nnmulcl  9275  zaddcllempos  9631  zaddcllemneg  9633  nn0n0n1ge2b  9675  fzind  9711  fnn0ind  9712  uzaddcl  9936  elpq  9999  uzsubsubfz  10401  elfz1b  10446  elfz0ubfz0  10481  fz0fzdiffz0  10486  elfzmlbp  10488  fzofzim  10549  elfzom1elp1fzo  10569  elfzom1p1elfzo  10581  ssfzo12bi  10592  modfzo0difsn  10781  seq3val  10846  seqvalcd  10847  expcllem  10936  expap0  10955  apexp1  11105  faclbnd  11128  faclbnd6  11131  fihashf1rn  11176  omgadd  11191  hashfzp1  11214  hashmap  11217  seq3coll  11239  fundm2domnop0  11245  lswlgt0cl  11302  ccatsymb  11315  swrdnd  11376  swrd0g  11377  swrdspsleq  11384  pfxsuff1eqwrdeq  11416  swrdswrdlem  11421  swrdswrd  11422  wrd2ind  11440  pfxccatin12lem2a  11444  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  pfxccat3a  11455  swrdccat3blem  11456  cjexp  11603  r19.29uz  11702  resqrexlemover  11720  resqrexlemlo  11723  resqrexlemcalc3  11726  absexp  11789  fimaxre2  11937  climshft  12014  climub  12054  climserle  12055  sumfct  12084  isumss2  12104  binom  12195  bcxmas  12200  clim2prod  12250  prodfap0  12256  prodfrecap  12257  prodfct  12298  demoivreALT  12485  dvdsdivcl  12561  dvdsfac  12571  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  m1exp1  12612  nn0o  12618  flodddiv4  12647  gcdneg  12703  bezoutlemmain  12719  dfgcd2  12735  gcdmultiple  12741  nnwosdc  12760  alginv  12769  cncongr1  12825  prmdvdsexp  12870  prmndvdsfaclt  12878  dfgrp2  13782  srgmulgass  14232  lmodvsmmulgdi  14597  lmodfopnelem1  14598  rmodislmodlem  14624  cnfldmulg  14850  cnfldexp  14851  clsss  15109  xmettri2  15352  mettri  15364  metss  15485  plycolemc  15749  zabsle1  15998  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  2lgslem1a1  16085  incistruhgr  16211  umgrislfupgrenlem  16251  uhgr2edg  16327  usgredg2vlem2  16344  subgrfun  16388  wlkl1loop  16479  wlkres  16500  clwwlkccatlem  16521  isclwwlknx  16537  clwwlkext2edg  16543  clwwlknonel  16553  clwwlknonex2lem2  16559  clwwlknun  16562  depindlem2  16628  depindlem3  16629  bdssexg  16800  bj-findis  16875  nninfalllem1  16912  nninfsellemdc  16914  redc0  16968