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  2836  2gencl  2837  vtocl4g  2876  vtocl4ga  2877  rspccva  2910  indifdir  3465  sseq0  3538  minel  3558  r19.2m  3583  r19.2mOLD  3584  elelpwi  3668  ssuni  3920  disjiun  4088  trintssm  4208  ssexg  4233  pofun  4415  sowlin  4423  2optocl  4809  3optocl  4810  ssrelrn  4928  elrnmpt1  4989  resieq  5029  fnun  5445  fss  5501  fun  5516  dmfex  5535  fvelimab  5711  mptfvex  5741  fmptco  5821  fnressn  5848  fressnfv  5849  fvtp2g  5871  fvtp3g  5872  fnex  5884  funfvima3  5898  isores3  5966  f1o2ndf1  6402  funsssuppss  6436  reldmtpos  6462  smores  6501  tfrlem7  6526  tfrlemi1  6541  tfrexlem  6543  tfrcl  6573  frecrdg  6617  nnacl  6691  nnmcl  6692  nnmsucr  6699  nntri3or  6704  nnaword  6722  nnaordex  6739  2ecoptocl  6835  ssct  7043  enm  7047  xpf1o  7073  ac6sfi  7130  f1dmvrnfibi  7186  f1vrnfibi  7187  updjud  7324  enumct  7357  nnnninfeq  7370  exmidontriimlem4  7482  exmidontriim  7483  elni2  7577  ax1rid  8140  negf1o  8603  mulgt1  9085  lbreu  9167  nnaddcl  9205  nnmulcl  9206  zaddcllempos  9560  zaddcllemneg  9562  nn0n0n1ge2b  9603  fzind  9639  fnn0ind  9640  uzaddcl  9864  elpq  9927  uzsubsubfz  10327  elfz1b  10370  elfz0ubfz0  10405  fz0fzdiffz0  10410  elfzmlbp  10412  fzofzim  10473  elfzom1elp1fzo  10493  elfzom1p1elfzo  10505  ssfzo12bi  10516  modfzo0difsn  10703  seq3val  10768  seqvalcd  10769  expcllem  10858  expap0  10877  apexp1  11026  faclbnd  11049  faclbnd6  11052  fihashf1rn  11096  omgadd  11111  hashfzp1  11134  seq3coll  11152  fundm2domnop0  11158  lswlgt0cl  11215  ccatsymb  11228  swrdnd  11289  swrd0g  11290  swrdspsleq  11297  pfxsuff1eqwrdeq  11329  swrdswrdlem  11334  swrdswrd  11335  wrd2ind  11353  pfxccatin12lem2a  11357  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  pfxccat3a  11368  swrdccat3blem  11369  cjexp  11516  r19.29uz  11615  resqrexlemover  11633  resqrexlemlo  11636  resqrexlemcalc3  11639  absexp  11702  fimaxre2  11850  climshft  11927  climub  11967  climserle  11968  sumfct  11997  isumss2  12017  binom  12108  bcxmas  12113  clim2prod  12163  prodfap0  12169  prodfrecap  12170  prodfct  12211  demoivreALT  12398  dvdsdivcl  12474  dvdsfac  12484  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  m1exp1  12525  nn0o  12531  flodddiv4  12560  gcdneg  12616  bezoutlemmain  12632  dfgcd2  12648  gcdmultiple  12654  nnwosdc  12673  alginv  12682  cncongr1  12738  prmdvdsexp  12783  prmndvdsfaclt  12791  dfgrp2  13673  srgmulgass  14066  lmodvsmmulgdi  14402  lmodfopnelem1  14403  rmodislmodlem  14429  cnfldmulg  14655  cnfldexp  14656  clsss  14912  xmettri2  15155  mettri  15167  metss  15288  plycolemc  15552  zabsle1  15801  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  2lgslem1a1  15888  incistruhgr  16014  umgrislfupgrenlem  16054  uhgr2edg  16130  usgredg2vlem2  16147  subgrfun  16191  wlkl1loop  16282  wlkres  16303  clwwlkccatlem  16324  isclwwlknx  16340  clwwlkext2edg  16346  clwwlknonel  16356  clwwlknonex2lem2  16362  clwwlknun  16365  depindlem2  16431  depindlem3  16432  bdssexg  16603  bj-findis  16678  nninfalllem1  16717  nninfsellemdc  16719  redc0  16773