Theorem impcom 413

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpan9  516  anbiim  653  bianir  1074  19.29r  1907  19.41v  1982  19.41  2274  nfsb4t  2533  mo4  2596  2euexv  2661  2euex  2671  gencl  3498  2gencl  3499  vtocl2ga  3544  vtocl2gaf  3545  vtocl3gaf  3546  vtocl3ga  3547  vtocl4g  3548  vtocl4ga  3549  rspccva  3582  2reurex  3725  2reu1  3852  rexdifi  4104  r19.2z  4462  falseral0OLD  4478  elelpwi  4574  preqsnd  4826  prproe  4872  ssuni  4900  disji2  5095  disjiun  5099  disjxiun  5108  trintss  5239  ssexgOLD  5296  reusv2lem3  5373  propeqop  5492  otiunsndisj  5505  rexopabb  5514  pofun  5589  solin  5598  2optocl  5759  3optocl  5760  ssrelrn  5886  elrnmpt1  5952  resieq  5991  imadifssranOLD  6205  reuop  6298  fnun  6653  fss  6726  fun  6744  fvelimab  6957  fvmptss  7006  fvn0ssdmfun  7073  fvcofneq  7092  fmptco  7129  funsndifnop  7154  fnressn  7161  fressnfv  7163  fmptsng  7172  fvtp2g  7203  fvtp3g  7204  tpres  7206  fnex  7222  funfvima3  7241  fvf1pr  7314  isores3  7342  tfisg  7856  dmfex  7908  opreuopreu  8037  releldmdifi  8048  funeldmdif  8051  el2mpocsbcl  8086  f1o2ndf1  8123  frxp  8128  fnse  8135  frxp2  8146  frxp3  8153  poseq  8160  ressuppssdif  8187  funsssuppss  8192  mpoxopxnop0  8217  reldmtpos  8236  frrlem8  8296  fpr2a  8305  smores  8345  tfrlem7  8376  tz7.48-2  8435  tz7.49  8438  oacl  8526  omcl  8527  oecl  8528  oarec  8553  oewordri  8584  oeworde  8585  oelim2  8587  oeoa  8589  oeoelem  8590  oeoe  8591  nnacl  8603  nnmcl  8604  nnecl  8605  nnmsucr  8617  naddoa  8695  brinxper  8730  2ecoptocl  8812  fsetprcnex  8865  undifixp  8938  funen1cnv  9032  xpf1o  9134  limensuc  9149  unfi  9162  en1eqsn  9242  ac6sfi  9251  frfi  9252  difinf  9278  f1dmvrnfibi  9305  f1vrnfibi  9306  suppeqfsuppbi  9346  elfiun  9397  dffi3  9398  infsupprpr  9473  xpwdomg  9554  infdiffi  9634  ttrclselem2  9702  epfrs  9707  frmin  9728  frr2  9739  rankxpsuc  9861  updjud  9936  tskwe  9952  infxpenlem  10013  fseqenlem1  10024  kmlem2  10151  nnadju  10197  cff1  10257  cflim2  10262  sornom  10276  infpssrlem4  10305  fin23lem26  10324  fin23lem30  10341  fin23lem34  10345  isf32lem11  10362  fin67  10394  isfin7-2  10395  fin1a2lem10  10408  axcc2lem  10435  axdc2lem  10447  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  iunfo  10538  tsk0  10763  gruina  10818  grur1a  10819  mulcanenq  10960  reclem2pr  11048  supsrlem  11111  supsr  11112  ax1rid  11161  negf1o  11659  lbreu  12180  nnindd  12268  nnaddcl  12271  nnmulcl  12272  nn0n0n1ge2b  12588  nn0indd  12709  fzind  12710  fnn0ind  12711  uzaddcl  12944  uzinfi  12968  nn01to3  12981  elpq  13015  xmulasslem2  13324  supxrunb1  13361  supxrunb2  13362  infmremnf  13386  infmrp1  13387  uzsubsubfz  13591  fzdif1  13650  elfz0ubfz0  13677  fz0fzdiffz0  13682  elfzmlbp  13684  fzofzim  13755  elfzom1elp1fzo  13778  ssfzo12bi  13807  fzoopth  13808  fzonfzoufzol  13817  elfznelfzob  13820  injresinjlem  13836  injresinj  13837  modaddmodup  13988  modfzo0difsn  13997  modsumfzodifsn  13998  addmodlteq  14000  om2uzlti  14004  fsequb  14029  ssnn0fi  14039  ser1const  14112  expcllem  14126  expeq0  14146  expmordi  14221  expnngt1  14295  faclbnd  14344  hashf1rn  14406  hashgadd  14431  hashunx  14440  hashnn0n0nn  14445  hashgt0elex  14455  hashss  14463  hashfzp1  14486  hashxp  14489  hashmap  14490  hashimarni  14496  seqcoll  14519  hash2exprb  14526  hashge2el2difr  14536  elss2prb  14543  hashdifsnp1  14561  fi1uzind  14562  brfi1indALT  14565  lswlgt0cl  14624  swrdnd  14714  swrdnnn0nd  14716  swrdnd0  14717  swrd0  14718  swrdsbslen  14724  swrdspsleq  14725  pfxsuff1eqwrdeq  14758  swrdswrdlem  14763  swrdswrd  14764  wrd2ind  14782  pfxccatin12lem2a  14786  swrdccatin2  14788  pfxccatin12lem2  14790  pfxccatin12lem3  14791  pfxccatin12  14792  pfxccat3  14793  swrdccat  14794  pfxccat3a  14797  swrdccat3blem  14798  repswswrd  14845  repswrevw  14848  cshwmodn  14856  cshwsublen  14857  cshwidxmod  14864  cshwidxmodr  14865  cshf1  14871  2cshw  14874  cshweqrep  14882  cshw1  14883  2cshwcshw  14886  cshwcshid  14888  cshwcsh2id  14889  wrdlen2i  15003  2swrd2eqwrdeq  15014  wwlktovfo  15019  relexpsucnnl  15091  rtrclreclem3  15121  rtrclreclem4  15122  relexpindlem  15124  r19.29uz  15426  caubnd  15434  sqreu  15436  climshft  15651  climub  15737  climserle  15738  sumss  15798  sumss2  15800  modfsummods  15868  o1fsum  15888  binom  15907  climcndslem1  15926  climcndslem2  15927  cvgrat  15960  clim2prod  15965  prodfn0  15971  prodfrec  15972  ntrivcvgfvn0  15976  fprodn0  16056  fprodmodd  16074  fprodefsum  16171  demoivreALT  16279  ruclem8  16315  dvdsaddre2b  16387  dvdsdivcl  16396  dvdsfac  16406  oddnn02np1  16428  oddge22np1  16429  evennn02n  16430  evennn2n  16431  m1exp1  16456  nn0o  16463  pwp1fsum  16471  flodddiv4  16495  smu01lem  16565  dvdslegcd  16584  gcdneg  16602  dfgcd2  16626  seq1st  16651  alginv  16655  lcmf  16713  lcmftp  16716  lcmfunsnlem2lem2  16719  lcmfunsnlem  16721  lcmfun  16725  ncoprmgcdne1b  16730  coprmproddvdslem  16742  coprmproddvds  16743  cncongr1  16747  prmdvdsexp  16796  prmndvdsfaclt  16806  ncoprmlnprm  16809  fvprmselgcd1  17127  prmgaplem6  17138  prmgaplem7  17139  prmgaplem8  17140  cshwshashlem1  17177  setsstruct2  17256  setsstruct  17258  inveq  17853  catsubcat  17918  initoeu2lem0  18092  initoeu2lem1  18093  funcestrcsetclem8  18225  funcestrcsetclem9  18226  fthestrcsetc  18228  fullestrcsetc  18229  funcsetcestrclem9  18241  fthsetcestrc  18243  fullsetcestrc  18244  lubss  18591  lubel  18592  mgmpropd  18733  issstrmgm  18735  mgmb1mgm1  18737  mgmidpfod  18760  sgrpidmnd  18829  frmdgsum  18958  smndex1mndlem  19008  mgm2nsgrplem3  19019  dfgrp2  19073  cyccom  19318  gaass  19411  gsumwrev  19480  symgextf1lem  19534  symgextf1  19535  fvcosymgeq  19543  gsmsymgreq  19546  symgfixelsi  19549  pmtrprfv3  19568  symggen  19584  pmtrprfval  19601  gsumzres  20023  gsumpr  20069  gsumzunsnd  20070  srgmulgass  20343  srgbinom  20357  0ringnnzr  20673  rnghmsscmap  20779  rnghmsubcsetclem2  20781  rngcinv  20786  funcrngcsetc  20789  funcrngcsetcALT  20790  rhmsscmap  20808  rhmsubcsetclem2  20810  rhmsubcrngclem2  20816  funcringcsetc  20823  srhmsubc  20829  rhmsubclem4  20837  lmodvsmmulgdi  21068  lmodfopnelem1  21069  rmodislmodlem  21100  rngqiprngimfo  21491  cnfldmulg  21604  cnfldexp  21605  ofldchr  21776  psgndiflemB  21800  assamulgscm  22101  gsumply1subr  22443  gsummoncoe1  22518  pf1ind  22565  matmulcell  22652  mat1dimscm  22682  dmatmul  22704  dmatscmcl  22710  scmataddcl  22723  scmatsubcl  22724  scmatsgrp1  22729  mavmulsolcl  22758  ma1repveval  22778  1marepvmarrepid  22782  symgmatr01lem  22860  slesolvec  22886  cramerimplem2  22891  decpmatmullem  22978  pm2mpf1  23006  mp2pm2mplem4  23016  monmat2matmon  23031  chpscmat  23049  chpscmatgsumbin  23051  fvmptnn04ifb  23058  chfacfscmul0  23065  chfacfscmulgsum  23067  chfacfpmmul0  23069  chfacfpmmulgsum  23071  cpmadugsumlemF  23083  toprntopon  23132  clsss  23261  ntrss  23262  restntr  23389  cmpsublem  23606  cmpsub  23607  2ndcrest  23661  txindislem  23841  t0kq  24026  filufint  24128  fbflim2  24185  flftg  24204  alexsubALTlem4  24258  cnextfvval  24273  ustuqtop4  24452  xmettri2  24548  mettri  24560  metss  24716  tngngp3  24864  clmvscom  25300  lmmbr  25468  caublcls  25519  lmcau  25523  ovolunlem1a  25706  nulmbl2  25746  voliunlem1  25760  iunmbl  25763  volsup  25766  dvlip  26203  dvfsumle  26231  degltlem1  26280  ply1divex  26345  plyco  26449  dgrnznn  26455  dvnply2  26499  plydivex  26509  aannenlem2  26543  aaliou3lem2  26557  ulmcau  26609  zabsle1  27511  gausslemma2dlem1a  27580  gausslemma2dlem2  27582  gausslemma2dlem3  27583  gausslemma2dlem4  27584  2lgslem1a1  27604  2sqnn0  27653  2sqreulem1  27661  2sqreunnlem1  27664  dchrisumlem1  27704  dchrisumlem2  27705  dchrisumlem3  27706  qabvle  27840  ostthlem2  27843  ostth2lem2  27849  nosupbnd1lem5  27927  noinfbnd1lem5  27942  nocvxminlem  27998  lesrec  28043  madebdaylemold  28142  mulsuniflem  28393  precsexlem6  28456  precsexlem7  28457  precsexlem8  28458  precsexlem9  28459  abssge0  28489  noseqind  28536  om2noseqlt  28543  om2noseqrdg  28548  n0addscl  28588  n0mulscl  28589  onsfi  28600  oldfib  28621  expscllem  28674  pw2cut2  28706  z12zsodd  28726  tgjustr  28794  axeuclidlem  29367  incistruhgr  29484  umgredgprv  29512  umgrpredgv  29545  usgredgprvALT  29603  uhgr2edg  29616  usgredg2vlem2  29634  lfuhgr1v0e  29662  subgrfun  29689  umgrres1lem  29718  upgrres1  29721  fusgrfis  29738  uhgrnbgr0nb  29762  nbgr1vtx  29766  nb3grprlem1  29788  uvtx01vtx  29805  fusgrn0degnn0  29907  vtxdginducedm1lem4  29950  finsumvtxdg2size  29958  wlkl1loop  30045  wlkres  30076  lfgrwlknloop  30099  pthdadjvtx  30140  dfpth2  30141  upgr2pthnlp  30145  upgrwlkdvdelem  30149  upgrwlkdvde  30150  uhgrwkspthlem2  30167  usgr2trlspth  30174  usgr2pth  30177  pthdlem2lem  30180  cyclnumvtx  30215  lfgrn1cycl  30221  uspgrn2crct  30224  crctcshwlkn0lem3  30228  crctcshwlkn0lem4  30229  crctcshwlkn0lem5  30230  iswspthsnon  30272  wlkiswwlks1  30283  wlklnwwlkln1  30284  wlkiswwlks2  30291  wlkiswwlksupgr2  30293  wlklnwwlkln2lem  30298  wlknwwlksnbij  30304  wwlksnred  30308  wwlksnext  30309  wwlksnredwwlkn  30311  wwlksnredwwlkn0  30312  wwlksnextfun  30314  wwlksnextinj  30315  wwlksnextsurj  30316  wspthsnonn0vne  30333  wspn0  30340  wwlks2onv  30369  elwwlks2  30385  elwspths2spth  30386  rusgrnumwwlk  30394  clwwlkccatlem  30407  clwlkclwwlklem2a1  30410  clwlkclwwlklem2fv2  30414  clwlkclwwlklem2a4  30415  clwlkclwwlklem2a  30416  clwlkclwwlklem2  30418  clwlkclwwlkf1lem3  30424  clwwisshclwwslem  30432  clwwisshclwwsn  30434  erclwwlktr  30440  isclwwlknx  30454  clwwlkinwwlk  30458  clwwlkel  30464  clwwlkf  30465  clwwlkf1  30467  clwwlkfo  30468  clwwlkext2edg  30474  wwlksext2clwwlk  30475  wwlksubclwwlk  30476  clwwlknscsh  30480  erclwwlkntr  30489  eleclclwwlkn  30494  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  clwwlknon0  30511  clwwlknonel  30513  clwwlknon1  30515  clwwlknonwwlknonb  30524  clwwlknonex2lem2  30526  clwwlknun  30530  clwwlkvbij  30531  upgr3v3e3cycl  30602  uhgr3cyclex  30604  upgr4cycl4dv4e  30607  eulerpath  30663  eucrctshift  30665  eucrct2eupth  30667  1to2vfriswmgr  30701  1to3vfriswmgr  30702  3cyclfrgrrn1  30707  4cycl2vnunb  30712  frgrwopreglem2  30735  frgrwopreglem3  30736  frgrwopreglem5ALT  30744  fusgr2wsp2nb  30756  2clwwlk2clwwlklem  30768  2clwwlk2clwwlk  30772  numclwwlk1lem2f1  30779  numclwwlk1lem2fo  30780  numclwwlk1  30783  clwwlknonclwlknonf1o  30784  dlwwlknondlwlknonf1o  30787  numclwlk1  30793  numclwlk2lem2f  30799  numclwlk2lem2f1o  30801  numclwwlk5  30810  frgrreg  30816  frgrregord013  30817  friendship  30821  nsnlplig  30904  nsnlpligALT  30905  isgrpo  30920  vcdi  30988  vcdir  30989  vcass  30990  nmosetre  31187  hlim2  31615  shscli  31740  chintcli  31754  dfch2  31830  spansncvi  32075  nmopsetretALT  32286  nmfnsetre  32300  lnopl  32337  lnfnl  32354  pjss2coi  32587  pjorthcoi  32592  pjscji  32593  pjssdif2i  32597  pjclem4a  32621  pj3lem1  32629  strlem5  32678  hstrlem5  32686  cvmdi  32747  mdslmd3i  32755  atcv1  32803  atcvat4i  32820  cdj3lem2a  32859  cdj3lem3a  32862  opreu2reuALT  32894  iuninc  32976  disji2f  32993  disjif2  32997  fmptcof2  33073  xrsmulgzz  33393  1arithufdlem3  33900  esumfzf  34523  issgon  34577  voliune  34684  volfiniune  34685  rrvsum  34909  bnj228  35189  bnj1294  35270  bnj229  35337  bnj607  35369  bnj908  35384  bnj953  35392  bnj1118  35437  bnj1174  35456  bnj1388  35486  rankfilimbi  35553  r1filimi  35555  trssfir1om  35565  trssfir1omregs  35606  acycgrsubgr  35687  cvmliftlem15  35827  satfsschain  35893  satfdm  35898  satf0op  35906  fmla0xp  35912  gonarlem  35923  goalrlem  35925  satffunlem1lem1  35931  satffunlem2lem1  35933  dmopab3rexdif  35934  satefvfmla0  35947  prv1n  35960  iprodefisumlem  36269  faclimlem1  36272  dfon2lem6  36315  idinside  36613  onsucconni  37005  axuntco  37047  ttcmin  37064  elttctr  37073  dfttc2g  37074  mh-inf3f1  37109  bj-cbvew  37321  axc11n11r  37365  bj-brrelex12ALT  37760  bj-snmoore  37812  bj-finsumval0  37986  exlimim  38045  exellim  38047  icoreclin  38060  difunieq  38077  fvineqsneq  38115  pibt2  38120  wl-spae  38233  wl-aleq  38247  fin2so  38315  matunitlindf  38326  poimirlem4  38332  poimirlem26  38354  itg2addnclem  38379  upixp  38438  welb  38445  sdclem2  38451  metf1o  38464  sstotbnd3  38485  isbndx  38491  ismtycnv  38511  heiborlem4  38523  bfplem1  38531  opidonOLD  38561  grpomndo  38584  eldisjdmqsim2  39523  ax12eq  39773  ax12el  39774  cvrat4  40275  nn0addcom  43294  nn0mulcom  43298  mzpexpmpt  43534  diophren  43598  rmxypos  43732  jm2.17a  43745  jm2.17b  43746  rmygeid  43749  jm2.18  43773  jm2.25  43784  jm2.15nn0  43788  jm2.16nn0  43789  pwslnm  43879  isnumbasgrplem1  43886  dgraalem  43930  onuniintrab  44011  onsupuni  44014  onsupcl3  44018  naddonnn  44180  naddwordnexlem2  44183  relexpiidm  44488  relexpmulnn  44493  relexpmulg  44494  relexp01min  44497  relexp0a  44500  relexpxpmin  44501  clsk1indlem3  44827  grucollcld  45028  dvgrat  45080  radcnvrat  45082  sspwimpcf  45686  sspwimpcfVD  45687  e2ebindALT  45695  trfr  45729  et-sqrtnegnre  47645  fsetprcnexALT  47857  eu2ndop1stv  47920  afvfv0bi  47947  afveu  47948  afvres  47967  aovmpt4g  47996  ndmaovass  48001  ndmaovdistr  48002  afv2orxorb  48023  afv2eu  48033  imarnf1pr  48077  nltle2tri  48108  fzopredsuc  48119  subsubelfzo0  48122  2ffzoeq  48123  2tceilhalfelfzo1  48131  m1modmmod  48159  smonoord  48172  elsetpreimafvssdm  48193  iccpartres  48225  iccpartiltu  48229  iccpartigtl  48230  iccpartgt  48234  icceuelpartlem  48242  fargshiftf1  48248  ichnreuop  48279  ichreuopeq  48280  elsprel  48282  sprsymrelfo  48304  prproropf1olem4  48313  paireqne  48318  sbcpr  48328  reupr  48329  goldbachth  48357  fmtnoprmfac1  48375  fmtnoprmfac2  48377  prmdvdsfmtnof1lem2  48395  lighneallem2  48416  lighneallem4  48420  requad2  48446  even3prm2  48542  fpprwpprb  48563  gbegt5  48584  sbgoldbwt  48600  sbgoldbm  48607  nnsum3primesgbe  48615  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  bgoldbtbndlem2  48629  bgoldbtbndlem3  48630  bgoldbtbndlem4  48631  bgoldbtbnd  48632  isubgredg  48689  grimuhgr  48710  clnbgrgrim  48757  grtriprop  48764  cycl3grtrilem  48769  cycl3grtri  48770  gpgusgralem  48879  gpgedgvtx0  48884  gpgedgvtx1  48885  gpgcubic  48902  gpg5nbgr3star  48904  gpgprismgr4cycllem3  48920  upgrwlkupwlk  48963  uspgropssxp  48967  uspgrsprfo  48971  isassintop  49032  lidldomn1  49053  2zlidl  49062  2zrngamgm  49067  2zrngmmgm  49074  rngccatidALTV  49094  rngcinvALTV  49098  rhmsubcALTVlem4  49106  funcringcsetcALTV2lem9  49120  ringccatidALTV  49128  srhmsubcALTV  49147  lmodvsmdi  49216  ply1mulgsumlem1  49223  ply1mulgsumlem2  49224  lincdifsn  49261  lincsumcl  49268  lincscmcl  49269  lincext3  49293  lindslinindsimp1  49294  lindslinindsimp2lem5  49299  snlindsntor  49308  lincresunit2  49315  lincresunit3lem2  49317  zgtp1leeq  49358  elbigo2  49389  fllog2  49405  digexp  49444  dig1  49445  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  1arymaptf1  49479  2arymaptf1  49490  rrxlinec  49573  eenglngeehlnm  49576  rrx2linest  49579  itsclc0yqsol  49601  itsclc0xyqsol  49605