Theorem impcom 407

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpan9  506  bianir  1059  19.29r  1876  19.41v  1951  19.41  2243  nfsb4t  2503  mo4  2566  2euexv  2631  2euex  2641  gencl  3471  2gencl  3472  vtocl2ga  3521  vtocl2gaf  3522  vtocl3gaf  3524  vtocl3ga  3526  vtocl4g  3528  vtocl4ga  3529  rspccva  3563  2reurex  3706  2reu1  3835  rexdifi  4090  sseq0  4343  r19.2z  4439  falseral0OLD  4455  elelpwi  4551  preqsnd  4802  prproe  4848  ssuni  4875  disji2  5069  disjiun  5073  disjxiun  5082  trintss  5211  ssexg  5264  reusv2lem3  5342  propeqop  5461  otiunsndisj  5474  rexopabb  5483  pofun  5557  solin  5566  2optocl  5727  3optocl  5728  ssrelrn  5849  elrnmpt1  5915  resieq  5955  imadifssran  6115  reuop  6257  fnun  6612  fss  6684  fun  6702  fvelimab  6912  fvmptss  6960  fvn0ssdmfun  7026  fvcofneq  7045  fmptco  7082  funsndifnop  7105  fnressn  7112  fressnfv  7114  fmptsng  7123  fvtp2g  7154  fvtp3g  7155  tpres  7156  fnex  7172  funfvima3  7191  fvf1pr  7262  isores3  7290  tfisg  7805  dmfex  7856  opreuopreu  7987  releldmdifi  7998  funeldmdif  8001  el2mpocsbcl  8035  f1o2ndf1  8072  frxp  8076  fnse  8083  frxp2  8094  frxp3  8101  poseq  8108  ressuppssdif  8135  funsssuppss  8140  mpoxopxnop0  8165  reldmtpos  8184  frrlem8  8243  fpr2a  8252  smores  8292  tfrlem7  8322  tz7.48-2  8381  tz7.49  8384  oacl  8470  omcl  8471  oecl  8472  oarec  8497  oewordri  8528  oeworde  8529  oelim2  8531  oeoa  8533  oeoelem  8534  oeoe  8535  nnacl  8547  nnmcl  8548  nnecl  8549  nnmsucr  8561  naddoa  8638  brinxper  8673  2ecoptocl  8755  fsetprcnex  8809  undifixp  8882  xpf1o  9077  limensuc  9092  unfi  9105  en1eqsn  9185  ac6sfi  9194  frfi  9195  difinf  9221  imafiOLD  9226  f1dmvrnfibi  9251  f1vrnfibi  9252  suppeqfsuppbi  9292  elfiun  9343  dffi3  9344  infsupprpr  9419  xpwdomg  9500  infdiffi  9579  ttrclselem2  9647  epfrs  9652  frmin  9673  frr2  9684  rankxpsuc  9806  updjud  9858  tskwe  9874  infxpenlem  9935  fseqenlem1  9946  kmlem2  10074  nnadju  10120  cff1  10180  cflim2  10185  sornom  10199  infpssrlem4  10228  fin23lem26  10247  fin23lem30  10264  fin23lem34  10268  isf32lem11  10285  fin67  10317  isfin7-2  10318  fin1a2lem10  10331  axcc2lem  10358  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  iunfo  10461  tsk0  10686  gruina  10741  grur1a  10742  mulcanenq  10883  reclem2pr  10971  supsrlem  11034  supsr  11035  ax1rid  11084  negf1o  11580  mulgt1OLD  12014  lbreu  12106  nnindd  12194  nnaddcl  12197  nnmulcl  12198  nn0n0n1ge2b  12506  nn0indd  12626  fzind  12627  fnn0ind  12628  uzaddcl  12854  uzinfi  12878  nn01to3  12891  elpq  12925  xmulasslem2  13234  supxrunb1  13271  supxrunb2  13272  infmremnf  13296  infmrp1  13297  uzsubsubfz  13500  fzdif1  13559  elfz0ubfz0  13586  fz0fzdiffz0  13591  elfzmlbp  13593  fzofzim  13664  elfzom1elp1fzo  13687  ssfzo12bi  13716  fzoopth  13717  fzonfzoufzol  13726  elfznelfzob  13729  injresinjlem  13745  injresinj  13746  modaddmodup  13896  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  om2uzlti  13912  fsequb  13937  ssnn0fi  13947  ser1const  14020  expcllem  14034  expeq0  14054  expmordi  14129  expnngt1  14203  faclbnd  14252  hashf1rn  14314  hashgadd  14339  hashunx  14348  hashnn0n0nn  14353  hashgt0elex  14363  hashss  14371  hashfzp1  14393  hashxp  14396  hashmap  14397  hashimarni  14403  seqcoll  14426  hash2exprb  14433  hashge2el2difr  14443  elss2prb  14450  hashdifsnp1  14468  fi1uzind  14469  brfi1indALT  14472  lswlgt0cl  14531  swrdnd  14617  swrdnnn0nd  14619  swrdnd0  14620  swrd0  14621  swrdsbslen  14627  swrdspsleq  14628  pfxsuff1eqwrdeq  14661  swrdswrdlem  14666  swrdswrd  14667  wrd2ind  14685  pfxccatin12lem2a  14689  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12lem3  14694  pfxccatin12  14695  pfxccat3  14696  swrdccat  14697  pfxccat3a  14700  swrdccat3blem  14701  repswswrd  14746  repswrevw  14749  cshwmodn  14757  cshwsublen  14758  cshwidxmod  14765  cshwidxmodr  14766  cshf1  14772  2cshw  14775  cshweqrep  14783  cshw1  14784  2cshwcshw  14787  cshwcshid  14789  cshwcsh2id  14790  wrdlen2i  14904  2swrd2eqwrdeq  14915  wwlktovfo  14920  relexpsucnnl  14992  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  r19.29uz  15313  caubnd  15321  sqreu  15323  climshft  15538  climub  15624  climserle  15625  sumss  15686  sumss2  15688  modfsummods  15756  o1fsum  15776  binom  15795  climcndslem1  15814  climcndslem2  15815  cvgrat  15848  clim2prod  15853  prodfn0  15859  prodfrec  15860  ntrivcvgfvn0  15864  fprodn0  15944  fprodmodd  15962  fprodefsum  16060  demoivreALT  16168  ruclem8  16204  dvdsaddre2b  16276  dvdsdivcl  16285  dvdsfac  16295  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  m1exp1  16345  nn0o  16352  pwp1fsum  16360  flodddiv4  16384  smu01lem  16454  dvdslegcd  16473  gcdneg  16491  dfgcd2  16515  seq1st  16540  alginv  16544  lcmf  16602  lcmftp  16605  lcmfunsnlem2lem2  16608  lcmfunsnlem  16610  lcmfun  16614  ncoprmgcdne1b  16619  coprmproddvdslem  16631  coprmproddvds  16632  cncongr1  16636  prmdvdsexp  16685  prmndvdsfaclt  16695  ncoprmlnprm  16698  fvprmselgcd1  17016  prmgaplem6  17027  prmgaplem7  17028  prmgaplem8  17029  cshwshashlem1  17066  setsstruct2  17144  setsstruct  17146  inveq  17741  catsubcat  17806  initoeu2lem0  17980  initoeu2lem1  17981  funcestrcsetclem8  18113  funcestrcsetclem9  18114  fthestrcsetc  18116  fullestrcsetc  18117  funcsetcestrclem9  18129  fthsetcestrc  18131  fullsetcestrc  18132  lubss  18479  lubel  18480  mgmpropd  18619  issstrmgm  18621  mgmb1mgm1  18623  sgrpidmnd  18707  frmdgsum  18830  smndex1mndlem  18880  mgm2nsgrplem3  18891  dfgrp2  18938  cyccom  19178  gaass  19272  gsumwrev  19341  symgextf1lem  19395  symgextf1  19396  fvcosymgeq  19404  gsmsymgreq  19407  symgfixelsi  19410  pmtrprfv3  19429  symggen  19445  pmtrprfval  19462  gsumzres  19884  gsumpr  19930  gsumzunsnd  19931  srgmulgass  20198  srgbinom  20212  0ringnnzr  20502  rnghmsscmap  20607  rnghmsubcsetclem2  20609  rngcinv  20614  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap  20636  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  funcringcsetc  20651  srhmsubc  20657  rhmsubclem4  20665  lmodvsmmulgdi  20892  lmodfopnelem1  20893  rmodislmodlem  20924  rngqiprngimfo  21299  cnfldmulg  21384  cnfldexp  21385  ofldchr  21556  psgndiflemB  21580  assamulgscm  21881  gsumply1subr  22197  gsummoncoe1  22273  pf1ind  22320  matmulcell  22410  mat1dimscm  22440  dmatmul  22462  dmatscmcl  22468  scmataddcl  22481  scmatsubcl  22482  scmatsgrp1  22487  mavmulsolcl  22516  ma1repveval  22536  1marepvmarrepid  22540  symgmatr01lem  22618  slesolvec  22644  cramerimplem2  22649  decpmatmullem  22736  pm2mpf1  22764  mp2pm2mplem4  22774  monmat2matmon  22789  chpscmat  22807  chpscmatgsumbin  22809  fvmptnn04ifb  22816  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  cpmadugsumlemF  22841  toprntopon  22890  clsss  23019  ntrss  23020  restntr  23147  cmpsublem  23364  cmpsub  23365  2ndcrest  23419  txindislem  23598  t0kq  23783  filufint  23885  fbflim2  23942  flftg  23961  alexsubALTlem4  24015  cnextfvval  24030  ustuqtop4  24209  xmettri2  24305  mettri  24317  metss  24473  tngngp3  24621  clmvscom  25057  lmmbr  25225  caublcls  25276  lmcau  25280  ovolunlem1a  25463  nulmbl2  25503  voliunlem1  25517  iunmbl  25520  volsup  25523  dvlip  25960  dvfsumle  25988  degltlem1  26037  ply1divex  26102  plyco  26206  dgrnznn  26212  dvnply2  26253  plydivex  26263  aannenlem2  26295  aaliou3lem2  26309  ulmcau  26360  zabsle1  27259  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  gausslemma2dlem4  27332  2lgslem1a1  27352  2sqnn0  27401  2sqreulem1  27409  2sqreunnlem1  27412  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  qabvle  27588  ostthlem2  27591  ostth2lem2  27597  nosupbnd1lem5  27676  noinfbnd1lem5  27691  nocvxminlem  27746  lesrec  27791  madebdaylemold  27890  mulsuniflem  28141  precsexlem6  28204  precsexlem7  28205  precsexlem8  28206  precsexlem9  28207  abssge0  28237  noseqind  28284  om2noseqlt  28291  om2noseqrdg  28296  n0addscl  28336  n0mulscl  28337  onsfi  28348  oldfib  28369  expscllem  28422  pw2cut2  28454  z12zsodd  28474  tgjustr  28542  axeuclidlem  29031  incistruhgr  29148  umgredgprv  29176  umgrpredgv  29209  usgredgprvALT  29264  uhgr2edg  29277  usgredg2vlem2  29295  lfuhgr1v0e  29323  subgrfun  29350  umgrres1lem  29379  upgrres1  29382  fusgrfis  29399  uhgrnbgr0nb  29423  nbgr1vtx  29427  nb3grprlem1  29449  uvtx01vtx  29466  fusgrn0degnn0  29568  vtxdginducedm1lem4  29611  finsumvtxdg2size  29619  wlkl1loop  29706  wlkres  29737  lfgrwlknloop  29756  pthdadjvtx  29796  dfpth2  29797  upgr2pthnlp  29800  upgrwlkdvdelem  29804  upgrwlkdvde  29805  uhgrwkspthlem2  29822  usgr2trlspth  29829  usgr2pth  29832  pthdlem2lem  29835  cyclnumvtx  29868  lfgrn1cycl  29873  uspgrn2crct  29876  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  iswspthsnon  29924  wlkiswwlks1  29935  wlklnwwlkln1  29936  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wlknwwlksnbij  29956  wwlksnred  29960  wwlksnext  29961  wwlksnredwwlkn  29963  wwlksnredwwlkn0  29964  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextsurj  29968  wspthsnonn0vne  29985  wspn0  29992  wwlks2onv  30021  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlk  30046  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlkf1lem3  30076  clwwisshclwwslem  30084  clwwisshclwwsn  30086  erclwwlktr  30092  isclwwlknx  30106  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  clwwlkfo  30120  clwwlkext2edg  30126  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwlknscsh  30132  erclwwlkntr  30141  eleclclwwlkn  30146  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknon0  30163  clwwlknonel  30165  clwwlknon1  30167  clwwlknonwwlknonb  30176  clwwlknonex2lem2  30178  clwwlknun  30182  clwwlkvbij  30183  upgr3v3e3cycl  30250  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  eulerpath  30311  eucrctshift  30313  eucrct2eupth  30315  1to2vfriswmgr  30349  1to3vfriswmgr  30350  3cyclfrgrrn1  30355  4cycl2vnunb  30360  frgrwopreglem2  30383  frgrwopreglem3  30384  frgrwopreglem5ALT  30392  fusgr2wsp2nb  30404  2clwwlk2clwwlklem  30416  2clwwlk2clwwlk  30420  numclwwlk1lem2f1  30427  numclwwlk1lem2fo  30428  numclwwlk1  30431  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  numclwlk1  30441  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  numclwwlk5  30458  frgrreg  30464  frgrregord013  30465  friendship  30469  nsnlplig  30552  nsnlpligALT  30553  isgrpo  30568  vcdi  30636  vcdir  30637  vcass  30638  nmosetre  30835  hlim2  31263  shscli  31388  chintcli  31402  dfch2  31478  spansncvi  31723  nmopsetretALT  31934  nmfnsetre  31948  lnopl  31985  lnfnl  32002  pjss2coi  32235  pjorthcoi  32240  pjscji  32241  pjssdif2i  32245  pjclem4a  32269  pj3lem1  32277  strlem5  32326  hstrlem5  32334  cvmdi  32395  mdslmd3i  32403  atcv1  32451  atcvat4i  32468  cdj3lem2a  32507  cdj3lem3a  32510  opreu2reuALT  32546  iuninc  32630  disji2f  32647  disjif2  32651  fmptcof2  32730  xrsmulgzz  33069  1arithufdlem3  33606  esumfzf  34213  issgon  34267  voliune  34373  volfiniune  34374  rrvsum  34598  bnj228  34878  bnj1294  34959  bnj229  35026  bnj607  35058  bnj908  35073  bnj953  35081  bnj1118  35126  bnj1174  35145  bnj1388  35175  funen1cnv  35231  rankfilimbi  35244  r1filimi  35246  trssfir1om  35255  trssfir1omregs  35280  acycgrsubgr  35340  cvmliftlem15  35480  satfsschain  35546  satfdm  35551  satf0op  35559  fmla0xp  35565  gonarlem  35576  goalrlem  35578  satffunlem1lem1  35584  satffunlem2lem1  35586  dmopab3rexdif  35587  satefvfmla0  35600  prv1n  35613  iprodefisumlem  35922  faclimlem1  35925  dfon2lem6  35968  idinside  36266  onsucconni  36619  axuntco  36661  ttcmin  36678  elttctr  36687  dfttc2g  36688  mh-inf3f1  36723  bj-cbvew  36936  axc11n11r  36980  bj-brrelex12ALT  37374  bj-snmoore  37425  bj-finsumval0  37599  exlimim  37658  exellim  37660  icoreclin  37673  difunieq  37690  fvineqsneq  37728  pibt2  37733  wl-spae  37846  wl-aleq  37860  fin2so  37928  matunitlindf  37939  poimirlem4  37945  poimirlem26  37967  itg2addnclem  37992  upixp  38050  welb  38057  sdclem2  38063  metf1o  38076  sstotbnd3  38097  isbndx  38103  ismtycnv  38123  heiborlem4  38135  bfplem1  38143  opidonOLD  38173  grpomndo  38196  eldisjdmqsim2  39137  ax12eq  39387  ax12el  39388  cvrat4  39889  nn0addcom  42907  nn0mulcom  42911  mzpexpmpt  43177  diophren  43241  rmxypos  43375  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.18  43416  jm2.25  43427  jm2.15nn0  43431  jm2.16nn0  43432  pwslnm  43522  isnumbasgrplem1  43529  dgraalem  43573  onuniintrab  43654  onsupuni  43657  onsupcl3  43661  naddonnn  43823  naddwordnexlem2  43826  relexpiidm  44131  relexpmulnn  44136  relexpmulg  44137  relexp01min  44140  relexp0a  44143  relexpxpmin  44144  clsk1indlem3  44470  grucollcld  44687  dvgrat  44739  radcnvrat  44741  sspwimpcf  45346  sspwimpcfVD  45347  e2ebindALT  45355  trfr  45389  et-sqrtnegnre  47301  fsetprcnexALT  47510  eu2ndop1stv  47573  afvfv0bi  47600  afveu  47601  afvres  47620  aovmpt4g  47649  ndmaovass  47654  ndmaovdistr  47655  afv2orxorb  47676  afv2eu  47686  imarnf1pr  47730  nltle2tri  47761  fzopredsuc  47772  subsubelfzo0  47775  2ffzoeq  47776  2tceilhalfelfzo1  47784  m1modmmod  47812  smonoord  47825  elsetpreimafvssdm  47846  iccpartres  47878  iccpartiltu  47882  iccpartigtl  47883  iccpartgt  47887  icceuelpartlem  47895  fargshiftf1  47901  ichnreuop  47932  ichreuopeq  47933  elsprel  47935  sprsymrelfo  47957  prproropf1olem4  47966  paireqne  47971  sbcpr  47981  reupr  47982  goldbachth  48010  fmtnoprmfac1  48028  fmtnoprmfac2  48030  prmdvdsfmtnof1lem2  48048  lighneallem2  48069  lighneallem4  48073  requad2  48099  even3prm2  48195  fpprwpprb  48216  gbegt5  48237  sbgoldbwt  48253  sbgoldbm  48260  nnsum3primesgbe  48268  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  isubgredg  48342  grimuhgr  48363  clnbgrgrim  48410  grtriprop  48417  cycl3grtrilem  48422  cycl3grtri  48423  gpgusgralem  48532  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgcubic  48555  gpg5nbgr3star  48557  gpgprismgr4cycllem3  48573  upgrwlkupwlk  48616  uspgropssxp  48620  uspgrsprfo  48624  isassintop  48686  lidldomn1  48707  2zlidl  48716  2zrngamgm  48721  2zrngmmgm  48728  rngccatidALTV  48748  rngcinvALTV  48752  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem9  48774  ringccatidALTV  48782  srhmsubcALTV  48801  lmodvsmdi  48855  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  lincdifsn  48900  lincsumcl  48907  lincscmcl  48908  lincext3  48932  lindslinindsimp1  48933  lindslinindsimp2lem5  48938  snlindsntor  48947  lincresunit2  48954  lincresunit3lem2  48956  zgtp1leeq  48997  elbigo2  49028  fllog2  49044  digexp  49083  dig1  49084  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  1arymaptf1  49118  2arymaptf1  49129  rrxlinec  49212  eenglngeehlnm  49215  rrx2linest  49218  itsclc0yqsol  49240  itsclc0xyqsol  49244