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  1737  19.41  1738  equtr2  1763  mopick  2165  2euex  2174  gencl  2854  2gencl  2855  vtocl4g  2894  vtocl4ga  2895  rspccva  2928  indifdir  3487  sseq0  3564  minel  3585  r19.2m  3611  r19.2mOLD  3612  elelpwi  3697  ssuni  3952  disjiun  4120  trintssm  4240  ssexg  4267  pofun  4452  sowlin  4460  2optocl  4847  3optocl  4848  ssrelrn  4967  elrnmpt1  5028  resieq  5068  fnun  5484  fss  5541  fun  5556  dmfex  5577  fvelimab  5753  mptfvex  5785  fmptco  5865  fnressn  5892  fressnfv  5893  fvtp2g  5915  fvtp3g  5916  fnex  5928  funfvima3  5942  isores3  6011  f1o2ndf1  6454  funsssuppss  6488  reldmtpos  6514  smores  6553  tfrlem7  6578  tfrlemi1  6593  tfrexlem  6595  tfrcl  6625  frecrdg  6669  nnacl  6743  nnmcl  6744  nnmsucr  6751  nntri3or  6756  nnaword  6774  nnaordex  6791  2ecoptocl  6887  ssct  7104  enm  7108  xpf1o  7134  ac6sfi  7192  f1dmvrnfibi  7248  f1vrnfibi  7249  suppeqfsuppbi  7285  updjud  7412  enumct  7445  nnnninfeq  7458  exmidontriimlem4  7570  exmidontriim  7571  elni2  7671  ax1rid  8234  negf1o  8699  mulgt1  9183  lbreu  9265  nnaddcl  9303  nnmulcl  9304  zaddcllempos  9660  zaddcllemneg  9662  nn0n0n1ge2b  9704  fzind  9740  fnn0ind  9741  uzaddcl  9965  elpq  10028  uzsubsubfz  10430  elfz1b  10475  elfz0ubfz0  10510  fz0fzdiffz0  10515  elfzmlbp  10517  fzofzim  10578  elfzom1elp1fzo  10598  elfzom1p1elfzo  10610  ssfzo12bi  10621  modfzo0difsn  10810  seq3val  10875  seqvalcd  10876  expcllem  10965  expap0  10984  apexp1  11134  faclbnd  11157  faclbnd6  11160  fihashf1rn  11205  omgadd  11220  hashfzp1  11243  hashmap  11246  seq3coll  11272  fundm2domnop0  11278  lswlgt0cl  11335  ccatsymb  11348  swrdnd  11409  swrd0g  11410  swrdspsleq  11417  pfxsuff1eqwrdeq  11449  swrdswrdlem  11454  swrdswrd  11455  wrd2ind  11473  pfxccatin12lem2a  11477  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  pfxccat3a  11488  swrdccat3blem  11489  cjexp  11636  r19.29uz  11736  resqrexlemover  11754  resqrexlemlo  11757  resqrexlemcalc3  11760  absexp  11823  fimaxre2  11971  climshft  12048  climub  12088  climserle  12089  sumfct  12118  isumss2  12138  binom  12229  bcxmas  12234  clim2prod  12284  prodfap0  12290  prodfrecap  12291  prodfct  12332  demoivreALT  12519  dvdsdivcl  12595  dvdsfac  12605  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  m1exp1  12646  nn0o  12652  flodddiv4  12681  gcdneg  12737  bezoutlemmain  12753  dfgcd2  12769  gcdmultiple  12775  nnwosdc  12794  alginv  12803  cncongr1  12859  prmdvdsexp  12904  prmndvdsfaclt  12912  dfgrp2  13809  srgmulgass  14267  lmodvsmmulgdi  14632  lmodfopnelem1  14633  rmodislmodlem  14659  cnfldmulg  14885  cnfldexp  14886  clsss  15142  xmettri2  15385  mettri  15397  metss  15518  plycolemc  15782  zabsle1  16032  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem3  16096  gausslemma2dlem4  16097  2lgslem1a1  16119  incistruhgr  16245  umgrislfupgrenlem  16285  uhgr2edg  16361  usgredg2vlem2  16378  subgrfun  16422  wlkl1loop  16513  wlkres  16534  clwwlkccatlem  16555  isclwwlknx  16571  clwwlkext2edg  16577  clwwlknonel  16587  clwwlknonex2lem2  16593  clwwlknun  16596  depindlem2  16662  depindlem3  16663  bdssexg  16844  bj-findis  16919  nninfalllem1  16956  nninfsellemdc  16958  redc0  17012