Theorem impcom 411

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 410	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpan9  510  bianir  1059  19.29r  1882  19.41v  1958  19.41  2235  nfsb4t  2502  mo4  2565  2euexv  2632  2euex  2642  raleqbidvv  3305  gencl  3437  2gencl  3438  vtocl2ga  3480  vtocl4g  3485  rspccva  3526  2reurex  3662  2reu1  3796  rexdifi  4046  sseq0  4300  r19.2z  4392  ralf0  4411  falseral0  4417  elelpwi  4511  preqsnd  4755  prproe  4803  ssuni  4832  disji2  5021  invdisjrab  5025  disjiun  5026  disjxiun  5036  trintss  5163  ssexg  5201  reusv2lem3  5278  propeqop  5375  otiunsndisj  5388  rexopabb  5394  pofun  5471  solin  5478  2optocl  5628  3optocl  5629  ssrelrn  5748  elrnmpt1  5812  resieq  5847  reuop  6136  funimaexg  6444  fnun  6468  fss  6540  fun  6559  fvelimab  6762  fvmptss  6808  fvn0ssdmfun  6873  fvcofneq  6890  fmptco  6922  funsndifnop  6944  fnressn  6951  fressnfv  6953  fvn0fvelrn  6956  fmptsng  6961  fvtp2g  6992  fvtp3g  6993  tpres  6994  fnex  7011  funfvima3  7030  isores3  7122  dmfex  7663  opreuopreu  7784  releldmdifi  7794  funeldmdif  7797  el2mpocsbcl  7831  f1o2ndf1  7869  frxp  7871  fnse  7878  ressuppssdif  7905  funsssuppss  7910  suppssOLD  7915  mpoxopxnop0  7935  reldmtpos  7954  frrlem8  8012  fpr2  8022  wfrfun  8043  wfrlem12  8044  smores  8067  tfrlem7  8097  tz7.48-2  8156  tz7.49  8159  oacl  8240  omcl  8241  oecl  8242  oarec  8268  oewordri  8298  oeworde  8299  oelim2  8301  oeoa  8303  oeoelem  8304  oeoe  8305  nnacl  8317  nnmcl  8318  nnecl  8319  nnmsucr  8331  2ecoptocl  8468  fsetprcnex  8521  undifixp  8593  ssct  8704  xpf1o  8786  limensuc  8801  unfi  8828  imafi  8830  ac6sfi  8893  frfi  8894  difinf  8919  f1dmvrnfibi  8938  f1vrnfibi  8939  suppeqfsuppbi  8977  elfiun  9024  dffi3  9025  infsupprpr  9098  xpwdomg  9179  infdiffi  9251  epfrs  9325  rankxpsuc  9463  updjud  9515  tskwe  9531  infxpenlem  9592  fseqenlem1  9603  kmlem2  9730  nnadju  9776  cff1  9837  cflim2  9842  sornom  9856  infpssrlem4  9885  fin23lem26  9904  fin23lem30  9921  fin23lem34  9925  isf32lem11  9942  fin67  9974  isfin7-2  9975  fin1a2lem10  9988  axcc2lem  10015  axdc2lem  10027  axdc3lem2  10030  axdc3lem4  10032  axdc4lem  10034  iunfo  10118  tsk0  10342  gruina  10397  grur1a  10398  mulcanenq  10539  reclem2pr  10627  supsrlem  10690  supsr  10691  ax1rid  10740  negf1o  11227  mulgt1  11656  lbreu  11747  nnindd  11815  nnaddcl  11818  nnmulcl  11819  nn0n0n1ge2b  12123  nn0indd  12239  fzind  12240  fnn0ind  12241  uzaddcl  12465  uzinfi  12489  nn01to3  12502  elpq  12536  xmulasslem2  12837  supxrunb1  12874  supxrunb2  12875  infmremnf  12898  infmrp1  12899  uzsubsubfz  13099  elfz0ubfz0  13181  fz0fzdiffz0  13186  elfzmlbp  13188  fzofzim  13254  elfzom1elp1fzo  13274  ssfzo12bi  13302  fzonfzoufzol  13310  elfznelfzob  13313  injresinjlem  13327  injresinj  13328  modaddmodup  13472  modfzo0difsn  13481  modsumfzodifsn  13482  addmodlteq  13484  om2uzlti  13488  fsequb  13513  ssnn0fi  13523  ser1const  13597  expcllem  13611  expeq0  13630  expmordi  13702  expnngt1  13773  faclbnd  13821  hashf1rn  13884  hashgadd  13909  hashunx  13918  hashnn0n0nn  13923  hashgt0elex  13933  hashss  13941  hashfzp1  13963  hashxp  13966  hashmap  13967  hashimarni  13973  seqcoll  13995  hash2exprb  14002  hashge2el2difr  14012  elss2prb  14018  hashdifsnp1  14027  fi1uzind  14028  brfi1indALT  14031  lswlgt0cl  14089  swrdnd  14184  swrdnnn0nd  14186  swrdnd0  14187  swrd0  14188  swrdsbslen  14194  swrdspsleq  14195  pfxsuff1eqwrdeq  14229  swrdswrdlem  14234  swrdswrd  14235  wrd2ind  14253  pfxccatin12lem2a  14257  swrdccatin2  14259  pfxccatin12lem2  14261  pfxccatin12lem3  14262  pfxccatin12  14263  pfxccat3  14264  swrdccat  14265  pfxccat3a  14268  swrdccat3blem  14269  repswswrd  14314  repswrevw  14317  cshwmodn  14325  cshwsublen  14326  cshwidxmod  14333  cshwidxmodr  14334  cshf1  14340  2cshw  14343  cshweqrep  14351  cshw1  14352  2cshwcshw  14355  cshwcshid  14357  cshwcsh2id  14358  wrdlen2i  14472  2swrd2eqwrdeq  14483  wwlktovfo  14490  relexpsucnnl  14558  rtrclreclem3  14588  rtrclreclem4  14589  relexpindlem  14591  r19.29uz  14879  caubnd  14887  sqreu  14889  climshft  15102  climub  15190  climserle  15191  sumss  15253  sumss2  15255  modfsummods  15320  o1fsum  15340  binom  15357  climcndslem1  15376  climcndslem2  15377  cvgrat  15410  clim2prod  15415  prodfn0  15421  prodfrec  15422  ntrivcvgfvn0  15426  fprodn0  15504  fprodmodd  15522  fprodefsum  15619  demoivreALT  15725  ruclem8  15761  dvdsaddre2b  15831  dvdsdivcl  15840  dvdsfac  15850  oddnn02np1  15872  oddge22np1  15873  evennn02n  15874  evennn2n  15875  m1exp1  15900  nn0o  15907  pwp1fsum  15915  flodddiv4  15937  smu01lem  16007  dvdslegcd  16026  gcdneg  16044  dfgcd2  16069  gcdmultipleOLD  16075  seq1st  16091  alginv  16095  lcmf  16153  lcmftp  16156  lcmfunsnlem2lem2  16159  lcmfunsnlem  16161  lcmfun  16165  ncoprmgcdne1b  16170  coprmproddvdslem  16182  coprmproddvds  16183  cncongr1  16187  prmdvdsexp  16235  prmndvdsfaclt  16245  ncoprmlnprm  16247  fvprmselgcd1  16561  prmgaplem6  16572  prmgaplem7  16573  prmgaplem8  16574  cshwshashlem1  16612  setsstruct2  16703  setsstruct  16705  inveq  17233  catsubcat  17299  initoeu2lem0  17473  initoeu2lem1  17474  funcestrcsetclem8  17608  funcestrcsetclem9  17609  fthestrcsetc  17611  fullestrcsetc  17612  funcsetcestrclem9  17624  fthsetcestrc  17626  fullsetcestrc  17627  lubss  17973  lubel  17974  issstrmgm  18079  mgmb1mgm1  18081  sgrpidmnd  18132  frmdgsum  18243  smndex1mndlem  18290  mgm2nsgrplem3  18301  dfgrp2  18346  cyccom  18564  gaass  18645  gsumwrev  18712  symgextf1lem  18766  symgextf1  18767  fvcosymgeq  18775  gsmsymgreq  18778  symgfixelsi  18781  pmtrprfv3  18800  symggen  18816  pmtrprfval  18833  gsumzres  19248  gsumpr  19294  gsumzunsnd  19295  srgmulgass  19500  srgbinom  19514  lmodvsmmulgdi  19888  lmodfopnelem1  19889  rmodislmodlem  19920  0ringnnzr  20261  cnfldmulg  20349  cnfldexp  20350  psgndiflemB  20516  assamulgscm  20815  gsumply1subr  21109  gsummoncoe1  21179  pf1ind  21225  matmulcell  21296  mat1dimscm  21326  dmatmul  21348  dmatscmcl  21354  scmataddcl  21367  scmatsubcl  21368  scmatsgrp1  21373  mavmulsolcl  21402  ma1repveval  21422  1marepvmarrepid  21426  symgmatr01lem  21504  slesolvec  21530  cramerimplem2  21535  decpmatmullem  21622  pm2mpf1  21650  mp2pm2mplem4  21660  monmat2matmon  21675  chpscmat  21693  chpscmatgsumbin  21695  fvmptnn04ifb  21702  chfacfscmul0  21709  chfacfscmulgsum  21711  chfacfpmmul0  21713  chfacfpmmulgsum  21715  cpmadugsumlemF  21727  toprntopon  21776  clsss  21905  ntrss  21906  restntr  22033  cmpsublem  22250  cmpsub  22251  2ndcrest  22305  txindislem  22484  t0kq  22669  filufint  22771  fbflim2  22828  flftg  22847  alexsubALTlem4  22901  cnextfvval  22916  ustuqtop4  23096  xmettri2  23192  mettri  23204  metss  23360  tngngp3  23508  clmvscom  23941  lmmbr  24109  caublcls  24160  lmcau  24164  ovolunlem1a  24347  nulmbl2  24387  voliunlem1  24401  iunmbl  24404  volsup  24407  dvlip  24844  dvfsumle  24872  degltlem1  24924  ply1divex  24988  plyco  25089  dgrnznn  25095  dvnply2  25134  plydivex  25144  aannenlem2  25176  aaliou3lem2  25190  ulmcau  25241  zabsle1  26131  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  gausslemma2dlem3  26203  gausslemma2dlem4  26204  2lgslem1a1  26224  2sqnn0  26273  2sqreulem1  26281  2sqreunnlem1  26284  dchrisumlem1  26324  dchrisumlem2  26325  dchrisumlem3  26326  qabvle  26460  ostthlem2  26463  ostth2lem2  26469  tgjustr  26519  axeuclidlem  27007  incistruhgr  27124  umgredgprv  27152  umgrpredgv  27185  usgredgprvALT  27237  uhgr2edg  27250  usgredg2vlem2  27268  lfuhgr1v0e  27296  subgrfun  27323  umgrres1lem  27352  upgrres1  27355  fusgrfis  27372  uhgrnbgr0nb  27396  nbgr1vtx  27400  nb3grprlem1  27422  uvtx01vtx  27439  fusgrn0degnn0  27541  vtxdginducedm1lem4  27584  finsumvtxdg2size  27592  wlkl1loop  27679  wlkres  27712  lfgrwlknloop  27731  pthdadjvtx  27771  upgr2pthnlp  27773  upgrwlkdvdelem  27777  upgrwlkdvde  27778  uhgrwkspthlem2  27795  usgr2trlspth  27802  usgr2pth  27805  pthdlem2lem  27808  lfgrn1cycl  27843  uspgrn2crct  27846  crctcshwlkn0lem3  27850  crctcshwlkn0lem4  27851  crctcshwlkn0lem5  27852  iswspthsnon  27894  wlkiswwlks1  27905  wlklnwwlkln1  27906  wlkiswwlks2  27913  wlkiswwlksupgr2  27915  wlklnwwlkln2lem  27920  wlknwwlksnbij  27926  wwlksnred  27930  wwlksnext  27931  wwlksnredwwlkn  27933  wwlksnredwwlkn0  27934  wwlksnextfun  27936  wwlksnextinj  27937  wwlksnextsurj  27938  wspthsnonn0vne  27955  wspn0  27962  wwlks2onv  27991  elwwlks2  28004  elwspths2spth  28005  rusgrnumwwlk  28013  clwwlkccatlem  28026  clwlkclwwlklem2a1  28029  clwlkclwwlklem2fv2  28033  clwlkclwwlklem2a4  28034  clwlkclwwlklem2a  28035  clwlkclwwlklem2  28037  clwlkclwwlkf1lem3  28043  clwwisshclwwslem  28051  clwwisshclwwsn  28053  erclwwlktr  28059  isclwwlknx  28073  clwwlkinwwlk  28077  clwwlkel  28083  clwwlkf  28084  clwwlkf1  28086  clwwlkfo  28087  clwwlkext2edg  28093  wwlksext2clwwlk  28094  wwlksubclwwlk  28095  clwwlknscsh  28099  erclwwlkntr  28108  eleclclwwlkn  28113  hashecclwwlkn1  28114  umgrhashecclwwlk  28115  clwwlknon0  28130  clwwlknonel  28132  clwwlknon1  28134  clwwlknonwwlknonb  28143  clwwlknonex2lem2  28145  clwwlknun  28149  clwwlkvbij  28150  upgr3v3e3cycl  28217  uhgr3cyclex  28219  upgr4cycl4dv4e  28222  eulerpath  28278  eucrctshift  28280  eucrct2eupth  28282  1to2vfriswmgr  28316  1to3vfriswmgr  28317  3cyclfrgrrn1  28322  4cycl2vnunb  28327  frgrwopreglem2  28350  frgrwopreglem3  28351  frgrwopreglem5ALT  28359  fusgr2wsp2nb  28371  2clwwlk2clwwlklem  28383  2clwwlk2clwwlk  28387  numclwwlk1lem2f1  28394  numclwwlk1lem2fo  28395  numclwwlk1  28398  clwwlknonclwlknonf1o  28399  dlwwlknondlwlknonf1o  28402  numclwlk1  28408  numclwlk2lem2f  28414  numclwlk2lem2f1o  28416  numclwwlk5  28425  frgrreg  28431  frgrregord013  28432  friendship  28436  nsnlplig  28516  nsnlpligALT  28517  isgrpo  28532  vcdi  28600  vcdir  28601  vcass  28602  nmosetre  28799  hlim2  29227  shscli  29352  chintcli  29366  dfch2  29442  spansncvi  29687  nmopsetretALT  29898  nmfnsetre  29912  lnopl  29949  lnfnl  29966  pjss2coi  30199  pjorthcoi  30204  pjscji  30205  pjssdif2i  30209  pjclem4a  30233  pj3lem1  30241  strlem5  30290  hstrlem5  30298  cvmdi  30359  mdslmd3i  30367  atcv1  30415  atcvat4i  30432  cdj3lem2a  30471  cdj3lem3a  30474  opreu2reuALT  30498  iuninc  30573  disji2f  30589  disjif2  30593  fmptcof2  30668  xrsmulgzz  30960  ofldchr  31186  esumfzf  31703  issgon  31757  voliune  31863  volfiniune  31864  rrvsum  32087  bnj228  32380  bnj1294  32464  bnj229  32531  bnj607  32563  bnj908  32578  bnj953  32586  bnj1118  32631  bnj1174  32650  bnj1388  32680  funen1cnv  32727  acycgrsubgr  32787  cvmliftlem15  32927  satfsschain  32993  satfdm  32998  satf0op  33006  fmla0xp  33012  gonarlem  33023  goalrlem  33025  satffunlem1lem1  33031  satffunlem2lem1  33033  dmopab3rexdif  33034  satefvfmla0  33047  prv1n  33060  iprodefisumlem  33375  faclimlem1  33378  dfon2lem6  33434  tfisg  33456  frxp2  33471  frxp3  33477  poseq  33482  frr2  33508  nosupbnd1lem5  33601  noinfbnd1lem5  33616  nocvxminlem  33658  nocvxmin  33659  slerec  33699  madebdaylemold  33764  idinside  34072  onsucconni  34312  axc11n11r  34551  bj-brrelex12ALT  34923  bj-snmoore  34968  bj-finsumval0  35140  exlimim  35199  exellim  35201  icoreclin  35214  difunieq  35231  fvineqsneq  35269  pibt2  35274  wl-spae  35366  wl-aleq  35380  fin2so  35450  matunitlindf  35461  poimirlem4  35467  poimirlem26  35489  itg2addnclem  35514  upixp  35573  welb  35580  sdclem2  35586  metf1o  35599  sstotbnd3  35620  isbndx  35626  ismtycnv  35646  heiborlem4  35658  bfplem1  35666  opidonOLD  35696  grpomndo  35719  ax12eq  36641  ax12el  36642  cvrat4  37143  mzpexpmpt  40211  diophren  40279  rmxypos  40413  jm2.17a  40426  jm2.17b  40427  rmygeid  40430  jm2.18  40454  jm2.25  40465  jm2.15nn0  40469  jm2.16nn0  40470  pwslnm  40563  isnumbasgrplem1  40570  dgraalem  40614  relexpiidm  40930  relexpmulnn  40935  relexpmulg  40936  relexp01min  40939  relexp0a  40942  relexpxpmin  40943  clsk1indlem3  41271  grucollcld  41492  dvgrat  41544  radcnvrat  41546  sspwimpcf  42154  sspwimpcfVD  42155  e2ebindALT  42163  fsetprcnexALT  44171  eu2ndop1stv  44232  afvfv0bi  44259  afveu  44260  afvres  44279  aovmpt4g  44308  ndmaovass  44313  ndmaovdistr  44314  afv2orxorb  44335  afv2eu  44345  imarnf1pr  44389  nltle2tri  44421  fzopredsuc  44431  subsubelfzo0  44434  fzoopth  44435  2ffzoeq  44436  smonoord  44439  elsetpreimafvssdm  44454  iccpartres  44486  iccpartiltu  44490  iccpartigtl  44491  iccpartgt  44495  icceuelpartlem  44503  fargshiftf1  44509  ichnreuop  44540  ichreuopeq  44541  elsprel  44543  sprsymrelfo  44565  prproropf1olem4  44574  paireqne  44579  sbcpr  44589  reupr  44590  goldbachth  44615  fmtnoprmfac1  44633  fmtnoprmfac2  44635  prmdvdsfmtnof1lem2  44653  lighneallem2  44674  lighneallem4  44678  requad2  44691  even3prm2  44787  fpprwpprb  44808  gbegt5  44829  sbgoldbwt  44845  sbgoldbm  44852  nnsum3primesgbe  44860  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbndlem4  44876  bgoldbtbnd  44877  isomuspgrlem1  44895  isomuspgrlem2d  44899  upgrwlkupwlk  44918  uspgropssxp  44922  uspgrsprfo  44926  mgmpropd  44945  isassintop  45020  lidldomn1  45095  lidlmmgm  45099  2zlidl  45108  2zrngamgm  45113  2zrngmmgm  45120  rnghmsscmap  45148  rnghmsubcsetclem2  45150  rngcinv  45155  rngccatidALTV  45163  rngcinvALTV  45167  funcrngcsetc  45172  funcrngcsetcALT  45173  rhmsscmap  45194  rhmsubcsetclem2  45196  rhmsubcrngclem2  45202  ringcinv  45206  funcringcsetc  45209  funcringcsetcALTV2lem9  45218  ringccatidALTV  45226  ringcinvALTV  45230  srhmsubc  45250  rhmsubclem4  45263  srhmsubcALTV  45268  rhmsubcALTVlem4  45281  lmodvsmdi  45334  ply1mulgsumlem1  45343  ply1mulgsumlem2  45344  lincdifsn  45381  lincsumcl  45388  lincscmcl  45389  lincext3  45413  lindslinindsimp1  45414  lindslinindsimp2lem5  45419  snlindsntor  45428  lincresunit2  45435  lincresunit3lem2  45437  zgtp1leeq  45478  m1modmmod  45483  elbigo2  45514  fllog2  45530  digexp  45569  dig1  45570  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  1arymaptf1  45604  2arymaptf1  45615  rrxlinec  45698  eenglngeehlnm  45701  rrx2linest  45704  itsclc0yqsol  45726  itsclc0xyqsol  45730