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  2159  2euex  2168  gencl  2846  2gencl  2847  vtocl4g  2886  vtocl4ga  2887  rspccva  2920  indifdir  3477  sseq0  3550  minel  3570  r19.2m  3596  r19.2mOLD  3597  elelpwi  3681  ssuni  3936  disjiun  4104  trintssm  4224  ssexg  4249  pofun  4433  sowlin  4441  2optocl  4827  3optocl  4828  ssrelrn  4947  elrnmpt1  5008  resieq  5048  fnun  5464  fss  5521  fun  5536  dmfex  5557  fvelimab  5733  mptfvex  5763  fmptco  5843  fnressn  5870  fressnfv  5871  fvtp2g  5893  fvtp3g  5894  fnex  5906  funfvima3  5920  isores3  5988  f1o2ndf1  6424  funsssuppss  6458  reldmtpos  6484  smores  6523  tfrlem7  6548  tfrlemi1  6563  tfrexlem  6565  tfrcl  6595  frecrdg  6639  nnacl  6713  nnmcl  6714  nnmsucr  6721  nntri3or  6726  nnaword  6744  nnaordex  6761  2ecoptocl  6857  ssct  7067  enm  7071  xpf1o  7097  ac6sfi  7155  f1dmvrnfibi  7211  f1vrnfibi  7212  suppeqfsuppbi  7248  updjud  7373  enumct  7406  nnnninfeq  7419  exmidontriimlem4  7531  exmidontriim  7532  elni2  7629  ax1rid  8192  negf1o  8655  mulgt1  9137  lbreu  9219  nnaddcl  9257  nnmulcl  9258  zaddcllempos  9614  zaddcllemneg  9616  nn0n0n1ge2b  9657  fzind  9693  fnn0ind  9694  uzaddcl  9918  elpq  9981  uzsubsubfz  10381  elfz1b  10424  elfz0ubfz0  10459  fz0fzdiffz0  10464  elfzmlbp  10466  fzofzim  10527  elfzom1elp1fzo  10547  elfzom1p1elfzo  10559  ssfzo12bi  10570  modfzo0difsn  10757  seq3val  10822  seqvalcd  10823  expcllem  10912  expap0  10931  apexp1  11080  faclbnd  11103  faclbnd6  11106  fihashf1rn  11151  omgadd  11166  hashfzp1  11189  hashmap  11192  seq3coll  11214  fundm2domnop0  11220  lswlgt0cl  11277  ccatsymb  11290  swrdnd  11351  swrd0g  11352  swrdspsleq  11359  pfxsuff1eqwrdeq  11391  swrdswrdlem  11396  swrdswrd  11397  wrd2ind  11415  pfxccatin12lem2a  11419  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  pfxccat3a  11430  swrdccat3blem  11431  cjexp  11578  r19.29uz  11677  resqrexlemover  11695  resqrexlemlo  11698  resqrexlemcalc3  11701  absexp  11764  fimaxre2  11912  climshft  11989  climub  12029  climserle  12030  sumfct  12059  isumss2  12079  binom  12170  bcxmas  12175  clim2prod  12225  prodfap0  12231  prodfrecap  12232  prodfct  12273  demoivreALT  12460  dvdsdivcl  12536  dvdsfac  12546  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  m1exp1  12587  nn0o  12593  flodddiv4  12622  gcdneg  12678  bezoutlemmain  12694  dfgcd2  12710  gcdmultiple  12716  nnwosdc  12735  alginv  12744  cncongr1  12800  prmdvdsexp  12845  prmndvdsfaclt  12853  dfgrp2  13740  srgmulgass  14133  lmodvsmmulgdi  14471  lmodfopnelem1  14472  rmodislmodlem  14498  cnfldmulg  14724  cnfldexp  14725  clsss  14983  xmettri2  15226  mettri  15238  metss  15359  plycolemc  15623  zabsle1  15872  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  2lgslem1a1  15959  incistruhgr  16085  umgrislfupgrenlem  16125  uhgr2edg  16201  usgredg2vlem2  16218  subgrfun  16262  wlkl1loop  16353  wlkres  16374  clwwlkccatlem  16395  isclwwlknx  16411  clwwlkext2edg  16417  clwwlknonel  16427  clwwlknonex2lem2  16433  clwwlknun  16436  depindlem2  16502  depindlem3  16503  bdssexg  16674  bj-findis  16749  nninfalllem1  16786  nninfsellemdc  16788  redc0  16842