Theorem impcom 412

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 33	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 411	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mpan9  515  anbiim  652  bianir  1074  19.29r  1904  19.41v  1979  19.41  2271  nfsb4t  2531  mo4  2594  2euexv  2659  2euex  2669  gencl  3496  2gencl  3497  vtocl2ga  3542  vtocl2gaf  3543  vtocl3gaf  3544  vtocl3ga  3545  vtocl4g  3546  vtocl4ga  3547  rspccva  3580  2reurex  3723  2reu1  3851  rexdifi  4104  r19.2z  4460  falseral0OLD  4476  elelpwi  4572  preqsnd  4824  prproe  4870  ssuni  4898  disji2  5093  disjiun  5097  disjxiun  5106  trintss  5237  ssexgOLD  5294  reusv2lem3  5371  propeqop  5490  otiunsndisj  5503  rexopabb  5512  pofun  5587  solin  5596  2optocl  5757  3optocl  5758  ssrelrn  5884  elrnmpt1  5950  resieq  5989  imadifssranOLD  6203  reuop  6294  fnun  6649  fss  6722  fun  6740  fvelimab  6953  fvmptss  7002  fvn0ssdmfun  7069  fvcofneq  7088  fmptco  7125  funsndifnop  7148  fnressn  7155  fressnfv  7157  fmptsng  7166  fvtp2g  7197  fvtp3g  7198  tpres  7199  fnex  7215  funfvima3  7234  fvf1pr  7305  isores3  7333  tfisg  7846  dmfex  7898  opreuopreu  8027  releldmdifi  8038  funeldmdif  8041  el2mpocsbcl  8076  f1o2ndf1  8113  frxp  8118  fnse  8125  frxp2  8136  frxp3  8143  poseq  8150  ressuppssdif  8177  funsssuppss  8182  mpoxopxnop0  8207  reldmtpos  8226  frrlem8  8286  fpr2a  8295  smores  8335  tfrlem7  8366  tz7.48-2  8425  tz7.49  8428  oacl  8516  omcl  8517  oecl  8518  oarec  8543  oewordri  8574  oeworde  8575  oelim2  8577  oeoa  8579  oeoelem  8580  oeoe  8581  nnacl  8593  nnmcl  8594  nnecl  8595  nnmsucr  8607  naddoa  8685  brinxper  8720  2ecoptocl  8802  fsetprcnex  8855  undifixp  8928  xpf1o  9123  limensuc  9138  unfi  9151  en1eqsn  9231  ac6sfi  9240  frfi  9241  difinf  9267  f1dmvrnfibi  9294  f1vrnfibi  9295  suppeqfsuppbi  9335  elfiun  9386  dffi3  9387  infsupprpr  9462  xpwdomg  9543  infdiffi  9623  ttrclselem2  9691  epfrs  9696  frmin  9717  frr2  9728  rankxpsuc  9850  updjud  9916  tskwe  9932  infxpenlem  9993  fseqenlem1  10004  kmlem2  10131  nnadju  10177  cff1  10237  cflim2  10242  sornom  10256  infpssrlem4  10285  fin23lem26  10304  fin23lem30  10321  fin23lem34  10325  isf32lem11  10342  fin67  10374  isfin7-2  10375  fin1a2lem10  10388  axcc2lem  10415  axdc2lem  10427  axdc3lem2  10430  axdc3lem4  10432  axdc4lem  10434  iunfo  10518  tsk0  10743  gruina  10798  grur1a  10799  mulcanenq  10940  reclem2pr  11028  supsrlem  11091  supsr  11092  ax1rid  11141  negf1o  11639  lbreu  12160  nnindd  12248  nnaddcl  12251  nnmulcl  12252  nn0n0n1ge2b  12568  nn0indd  12688  fzind  12689  fnn0ind  12690  uzaddcl  12923  uzinfi  12947  nn01to3  12960  elpq  12994  xmulasslem2  13303  supxrunb1  13340  supxrunb2  13341  infmremnf  13365  infmrp1  13366  uzsubsubfz  13570  fzdif1  13629  elfz0ubfz0  13656  fz0fzdiffz0  13661  elfzmlbp  13663  fzofzim  13734  elfzom1elp1fzo  13757  ssfzo12bi  13786  fzoopth  13787  fzonfzoufzol  13796  elfznelfzob  13799  injresinjlem  13815  injresinj  13816  modaddmodup  13966  modfzo0difsn  13975  modsumfzodifsn  13976  addmodlteq  13978  om2uzlti  13982  fsequb  14007  ssnn0fi  14017  ser1const  14090  expcllem  14104  expeq0  14124  expmordi  14199  expnngt1  14273  faclbnd  14322  hashf1rn  14384  hashgadd  14409  hashunx  14418  hashnn0n0nn  14423  hashgt0elex  14433  hashss  14441  hashfzp1  14464  hashxp  14467  hashmap  14468  hashimarni  14474  seqcoll  14497  hash2exprb  14504  hashge2el2difr  14514  elss2prb  14521  hashdifsnp1  14539  fi1uzind  14540  brfi1indALT  14543  lswlgt0cl  14602  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  swrd0  14692  swrdsbslen  14698  swrdspsleq  14699  pfxsuff1eqwrdeq  14732  swrdswrdlem  14737  swrdswrd  14738  wrd2ind  14756  pfxccatin12lem2a  14760  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12lem3  14765  pfxccatin12  14766  pfxccat3  14767  swrdccat  14768  pfxccat3a  14771  swrdccat3blem  14772  repswswrd  14817  repswrevw  14820  cshwmodn  14828  cshwsublen  14829  cshwidxmod  14836  cshwidxmodr  14837  cshf1  14843  2cshw  14846  cshweqrep  14854  cshw1  14855  2cshwcshw  14858  cshwcshid  14860  cshwcsh2id  14861  wrdlen2i  14975  2swrd2eqwrdeq  14986  wwlktovfo  14991  relexpsucnnl  15063  rtrclreclem3  15093  rtrclreclem4  15094  relexpindlem  15096  r19.29uz  15398  caubnd  15406  sqreu  15408  climshft  15623  climub  15709  climserle  15710  sumss  15771  sumss2  15773  modfsummods  15841  o1fsum  15861  binom  15880  climcndslem1  15899  climcndslem2  15900  cvgrat  15933  clim2prod  15938  prodfn0  15944  prodfrec  15945  ntrivcvgfvn0  15949  fprodn0  16029  fprodmodd  16047  fprodefsum  16144  demoivreALT  16252  ruclem8  16288  dvdsaddre2b  16360  dvdsdivcl  16369  dvdsfac  16379  oddnn02np1  16401  oddge22np1  16402  evennn02n  16403  evennn2n  16404  m1exp1  16429  nn0o  16436  pwp1fsum  16444  flodddiv4  16468  smu01lem  16538  dvdslegcd  16557  gcdneg  16575  dfgcd2  16599  seq1st  16624  alginv  16628  lcmf  16686  lcmftp  16689  lcmfunsnlem2lem2  16692  lcmfunsnlem  16694  lcmfun  16698  ncoprmgcdne1b  16703  coprmproddvdslem  16715  coprmproddvds  16716  cncongr1  16720  prmdvdsexp  16769  prmndvdsfaclt  16779  ncoprmlnprm  16782  fvprmselgcd1  17100  prmgaplem6  17111  prmgaplem7  17112  prmgaplem8  17113  cshwshashlem1  17150  setsstruct2  17229  setsstruct  17231  inveq  17826  catsubcat  17891  initoeu2lem0  18065  initoeu2lem1  18066  funcestrcsetclem8  18198  funcestrcsetclem9  18199  fthestrcsetc  18201  fullestrcsetc  18202  funcsetcestrclem9  18214  fthsetcestrc  18216  fullsetcestrc  18217  lubss  18564  lubel  18565  mgmpropd  18704  issstrmgm  18706  mgmb1mgm1  18708  sgrpidmnd  18792  frmdgsum  18916  smndex1mndlem  18966  mgm2nsgrplem3  18977  dfgrp2  19024  cyccom  19269  gaass  19362  gsumwrev  19431  symgextf1lem  19485  symgextf1  19486  fvcosymgeq  19494  gsmsymgreq  19497  symgfixelsi  19500  pmtrprfv3  19519  symggen  19535  pmtrprfval  19552  gsumzres  19974  gsumpr  20020  gsumzunsnd  20021  srgmulgass  20294  srgbinom  20308  0ringnnzr  20623  rnghmsscmap  20729  rnghmsubcsetclem2  20731  rngcinv  20736  funcrngcsetc  20739  funcrngcsetcALT  20740  rhmsscmap  20758  rhmsubcsetclem2  20760  rhmsubcrngclem2  20766  funcringcsetc  20773  srhmsubc  20779  rhmsubclem4  20787  lmodvsmmulgdi  21018  lmodfopnelem1  21019  rmodislmodlem  21050  rngqiprngimfo  21441  cnfldmulg  21554  cnfldexp  21555  ofldchr  21726  psgndiflemB  21750  assamulgscm  22051  gsumply1subr  22393  gsummoncoe1  22468  pf1ind  22515  matmulcell  22602  mat1dimscm  22632  dmatmul  22654  dmatscmcl  22660  scmataddcl  22673  scmatsubcl  22674  scmatsgrp1  22679  mavmulsolcl  22708  ma1repveval  22728  1marepvmarrepid  22732  symgmatr01lem  22810  slesolvec  22836  cramerimplem2  22841  decpmatmullem  22928  pm2mpf1  22956  mp2pm2mplem4  22966  monmat2matmon  22981  chpscmat  22999  chpscmatgsumbin  23001  fvmptnn04ifb  23008  chfacfscmul0  23015  chfacfscmulgsum  23017  chfacfpmmul0  23019  chfacfpmmulgsum  23021  cpmadugsumlemF  23033  toprntopon  23082  clsss  23211  ntrss  23212  restntr  23339  cmpsublem  23556  cmpsub  23557  2ndcrest  23611  txindislem  23790  t0kq  23975  filufint  24077  fbflim2  24134  flftg  24153  alexsubALTlem4  24207  cnextfvval  24222  ustuqtop4  24401  xmettri2  24497  mettri  24509  metss  24665  tngngp3  24813  clmvscom  25249  lmmbr  25417  caublcls  25468  lmcau  25472  ovolunlem1a  25655  nulmbl2  25695  voliunlem1  25709  iunmbl  25712  volsup  25715  dvlip  26152  dvfsumle  26180  degltlem1  26229  ply1divex  26294  plyco  26398  dgrnznn  26404  dvnply2  26448  plydivex  26458  aannenlem2  26492  aaliou3lem2  26506  ulmcau  26558  zabsle1  27460  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem3  27532  gausslemma2dlem4  27533  2lgslem1a1  27553  2sqnn0  27602  2sqreulem1  27610  2sqreunnlem1  27613  dchrisumlem1  27653  dchrisumlem2  27654  dchrisumlem3  27655  qabvle  27789  ostthlem2  27792  ostth2lem2  27798  nosupbnd1lem5  27876  noinfbnd1lem5  27891  nocvxminlem  27947  lesrec  27992  madebdaylemold  28091  mulsuniflem  28342  precsexlem6  28405  precsexlem7  28406  precsexlem8  28407  precsexlem9  28408  abssge0  28438  noseqind  28485  om2noseqlt  28492  om2noseqrdg  28497  n0addscl  28537  n0mulscl  28538  onsfi  28549  oldfib  28570  expscllem  28623  pw2cut2  28655  z12zsodd  28675  tgjustr  28743  axeuclidlem  29312  incistruhgr  29429  umgredgprv  29457  umgrpredgv  29490  usgredgprvALT  29545  uhgr2edg  29558  usgredg2vlem2  29576  lfuhgr1v0e  29604  subgrfun  29631  umgrres1lem  29660  upgrres1  29663  fusgrfis  29680  uhgrnbgr0nb  29704  nbgr1vtx  29708  nb3grprlem1  29730  uvtx01vtx  29747  fusgrn0degnn0  29849  vtxdginducedm1lem4  29892  finsumvtxdg2size  29900  wlkl1loop  29987  wlkres  30018  lfgrwlknloop  30037  pthdadjvtx  30077  dfpth2  30078  upgr2pthnlp  30081  upgrwlkdvdelem  30085  upgrwlkdvde  30086  uhgrwkspthlem2  30103  usgr2trlspth  30110  usgr2pth  30113  pthdlem2lem  30116  cyclnumvtx  30149  lfgrn1cycl  30154  uspgrn2crct  30157  crctcshwlkn0lem3  30161  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  iswspthsnon  30205  wlkiswwlks1  30216  wlklnwwlkln1  30217  wlkiswwlks2  30224  wlkiswwlksupgr2  30226  wlklnwwlkln2lem  30231  wlknwwlksnbij  30237  wwlksnred  30241  wwlksnext  30242  wwlksnredwwlkn  30244  wwlksnredwwlkn0  30245  wwlksnextfun  30247  wwlksnextinj  30248  wwlksnextsurj  30249  wspthsnonn0vne  30266  wspn0  30273  wwlks2onv  30302  elwwlks2  30318  elwspths2spth  30319  rusgrnumwwlk  30327  clwwlkccatlem  30340  clwlkclwwlklem2a1  30343  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwlkclwwlkf1lem3  30357  clwwisshclwwslem  30365  clwwisshclwwsn  30367  erclwwlktr  30373  isclwwlknx  30387  clwwlkinwwlk  30391  clwwlkel  30397  clwwlkf  30398  clwwlkf1  30400  clwwlkfo  30401  clwwlkext2edg  30407  wwlksext2clwwlk  30408  wwlksubclwwlk  30409  clwwlknscsh  30413  erclwwlkntr  30422  eleclclwwlkn  30427  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknon0  30444  clwwlknonel  30446  clwwlknon1  30448  clwwlknonwwlknonb  30457  clwwlknonex2lem2  30459  clwwlknun  30463  clwwlkvbij  30464  upgr3v3e3cycl  30531  uhgr3cyclex  30533  upgr4cycl4dv4e  30536  eulerpath  30592  eucrctshift  30594  eucrct2eupth  30596  1to2vfriswmgr  30630  1to3vfriswmgr  30631  3cyclfrgrrn1  30636  4cycl2vnunb  30641  frgrwopreglem2  30664  frgrwopreglem3  30665  frgrwopreglem5ALT  30673  fusgr2wsp2nb  30685  2clwwlk2clwwlklem  30697  2clwwlk2clwwlk  30701  numclwwlk1lem2f1  30708  numclwwlk1lem2fo  30709  numclwwlk1  30712  clwwlknonclwlknonf1o  30713  dlwwlknondlwlknonf1o  30716  numclwlk1  30722  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  numclwwlk5  30739  frgrreg  30745  frgrregord013  30746  friendship  30750  nsnlplig  30833  nsnlpligALT  30834  isgrpo  30849  vcdi  30917  vcdir  30918  vcass  30919  nmosetre  31116  hlim2  31544  shscli  31669  chintcli  31683  dfch2  31759  spansncvi  32004  nmopsetretALT  32215  nmfnsetre  32229  lnopl  32266  lnfnl  32283  pjss2coi  32516  pjorthcoi  32521  pjscji  32522  pjssdif2i  32526  pjclem4a  32550  pj3lem1  32558  strlem5  32607  hstrlem5  32615  cvmdi  32676  mdslmd3i  32684  atcv1  32732  atcvat4i  32749  cdj3lem2a  32788  cdj3lem3a  32791  opreu2reuALT  32823  iuninc  32905  disji2f  32922  disjif2  32926  fmptcof2  33002  xrsmulgzz  33329  1arithufdlem3  33836  esumfzf  34459  issgon  34513  voliune  34619  volfiniune  34620  rrvsum  34844  bnj228  35124  bnj1294  35205  bnj229  35272  bnj607  35304  bnj908  35319  bnj953  35327  bnj1118  35372  bnj1174  35391  bnj1388  35421  funen1cnv  35477  rankfilimbi  35495  r1filimi  35497  trssfir1om  35507  trssfir1omregs  35549  acycgrsubgr  35650  cvmliftlem15  35790  satfsschain  35856  satfdm  35861  satf0op  35869  fmla0xp  35875  gonarlem  35886  goalrlem  35888  satffunlem1lem1  35894  satffunlem2lem1  35896  dmopab3rexdif  35897  satefvfmla0  35910  prv1n  35923  iprodefisumlem  36232  faclimlem1  36235  dfon2lem6  36278  idinside  36576  onsucconni  36948  axuntco  36990  ttcmin  37007  elttctr  37016  dfttc2g  37017  mh-inf3f1  37052  bj-cbvew  37264  axc11n11r  37308  bj-brrelex12ALT  37703  bj-snmoore  37755  bj-finsumval0  37929  exlimim  37988  exellim  37990  icoreclin  38003  difunieq  38020  fvineqsneq  38058  pibt2  38063  wl-spae  38176  wl-aleq  38190  fin2so  38258  matunitlindf  38269  poimirlem4  38275  poimirlem26  38297  itg2addnclem  38322  upixp  38380  welb  38387  sdclem2  38393  metf1o  38406  sstotbnd3  38427  isbndx  38433  ismtycnv  38453  heiborlem4  38465  bfplem1  38473  opidonOLD  38503  grpomndo  38526  eldisjdmqsim2  39465  ax12eq  39715  ax12el  39716  cvrat4  40217  nn0addcom  43236  nn0mulcom  43240  mzpexpmpt  43476  diophren  43540  rmxypos  43674  jm2.17a  43687  jm2.17b  43688  rmygeid  43691  jm2.18  43715  jm2.25  43726  jm2.15nn0  43730  jm2.16nn0  43731  pwslnm  43821  isnumbasgrplem1  43828  dgraalem  43872  onuniintrab  43953  onsupuni  43956  onsupcl3  43960  naddonnn  44122  naddwordnexlem2  44125  relexpiidm  44430  relexpmulnn  44435  relexpmulg  44436  relexp01min  44439  relexp0a  44442  relexpxpmin  44443  clsk1indlem3  44769  grucollcld  44970  dvgrat  45022  radcnvrat  45024  sspwimpcf  45628  sspwimpcfVD  45629  e2ebindALT  45637  trfr  45671  et-sqrtnegnre  47587  fsetprcnexALT  47799  eu2ndop1stv  47862  afvfv0bi  47889  afveu  47890  afvres  47909  aovmpt4g  47938  ndmaovass  47943  ndmaovdistr  47944  afv2orxorb  47965  afv2eu  47975  imarnf1pr  48019  nltle2tri  48050  fzopredsuc  48061  subsubelfzo0  48064  2ffzoeq  48065  2tceilhalfelfzo1  48073  m1modmmod  48101  smonoord  48114  elsetpreimafvssdm  48135  iccpartres  48167  iccpartiltu  48171  iccpartigtl  48172  iccpartgt  48176  icceuelpartlem  48184  fargshiftf1  48190  ichnreuop  48221  ichreuopeq  48222  elsprel  48224  sprsymrelfo  48246  prproropf1olem4  48255  paireqne  48260  sbcpr  48270  reupr  48271  goldbachth  48299  fmtnoprmfac1  48317  fmtnoprmfac2  48319  prmdvdsfmtnof1lem2  48337  lighneallem2  48358  lighneallem4  48362  requad2  48388  even3prm2  48484  fpprwpprb  48505  gbegt5  48526  sbgoldbwt  48542  sbgoldbm  48549  nnsum3primesgbe  48557  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  bgoldbtbnd  48574  isubgredg  48631  grimuhgr  48652  clnbgrgrim  48699  grtriprop  48706  cycl3grtrilem  48711  cycl3grtri  48712  gpgusgralem  48821  gpgedgvtx0  48826  gpgedgvtx1  48827  gpgcubic  48844  gpg5nbgr3star  48846  gpgprismgr4cycllem3  48862  upgrwlkupwlk  48905  uspgropssxp  48909  uspgrsprfo  48913  isassintop  48975  lidldomn1  48996  2zlidl  49005  2zrngamgm  49010  2zrngmmgm  49017  rngccatidALTV  49037  rngcinvALTV  49041  rhmsubcALTVlem4  49049  funcringcsetcALTV2lem9  49063  ringccatidALTV  49071  srhmsubcALTV  49090  lmodvsmdi  49159  ply1mulgsumlem1  49166  ply1mulgsumlem2  49167  lincdifsn  49204  lincsumcl  49211  lincscmcl  49212  lincext3  49236  lindslinindsimp1  49237  lindslinindsimp2lem5  49242  snlindsntor  49251  lincresunit2  49258  lincresunit3lem2  49260  zgtp1leeq  49301  elbigo2  49332  fllog2  49348  digexp  49387  dig1  49388  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  1arymaptf1  49422  2arymaptf1  49433  rrxlinec  49516  eenglngeehlnm  49519  rrx2linest  49522  itsclc0yqsol  49544  itsclc0xyqsol  49548