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  1906  19.41v  1981  19.41  2271  nfsb4t  2528  mo4  2591  2euexv  2656  2euex  2666  gencl  3491  2gencl  3492  vtocl2ga  3537  vtocl2gaf  3538  vtocl3gaf  3539  vtocl3ga  3540  vtocl4g  3541  vtocl4ga  3542  rspccva  3575  2reurex  3717  2reu1  3845  rexdifi  4085  r19.2z  4454  falseral0OLD  4470  elelpwi  4566  preqsnd  4813  prproe  4832  ssuni  4892  disji2  5086  disjiun  5090  disjxiun  5099  trintss  5230  ssexgOLD  5285  reusv2lem3  5362  propeqop  5479  otiunsndisj  5493  rexopabb  5502  pofun  5577  solin  5586  2optocl  5748  3optocl  5749  ssrelrn  5877  elrnmpt1  5943  resieq  5982  imadifssranOLDOLD  6206  reuop  6299  fnun  6658  fss  6731  fun  6749  fvelimab  6962  fvmptss  7011  fvn0ssdmfun  7079  fvcofneq  7098  fmptco  7135  funsndifnop  7160  fnressn  7167  fressnfv  7169  fmptsng  7177  fvtp2g  7208  fvtp3g  7209  tpres  7211  fnex  7227  funfvima3  7246  fvf1pr  7319  isores3  7347  tfisg  7869  dmfex  7921  opreuopreu  8050  releldmdifi  8060  funeldmdif  8063  el2mpocsbcl  8100  f1o2ndf1  8139  frxp  8144  fnse  8156  frxp2  8167  frxp3  8174  poseq  8181  ressuppssdif  8209  funsssuppss  8214  mpoxopxnop0  8239  reldmtpos  8258  frrlem8  8318  fpr2a  8327  smores  8367  tfrlem7  8398  onelfvnef1  8456  tz7.48-2  8459  tz7.49  8462  oacl  8550  omcl  8551  oecl  8552  oarec  8577  oewordri  8608  oeworde  8609  oelim2  8611  oeoa  8613  oeoelem  8614  oeoe  8615  nnacl  8627  nnmcl  8628  nnecl  8629  nnmsucr  8641  naddoa  8719  brinxper  8754  2ecoptocl  8836  fsetprcnex  8891  undifixp  8969  funen1cnv  9063  xpf1o  9165  limensuc  9180  unfi  9193  en1eqsn  9273  ac6sfi  9282  frfi  9283  difinf  9310  f1dmvrnfibi  9337  f1vrnfibi  9338  suppeqfsuppbi  9378  elfiun  9429  dffi3  9430  infsupprpr  9505  xpwdomg  9586  infdiffi  9666  ttrclselem2  9734  epfrs  9739  frmin  9760  frr2  9771  rankxpsuc  9906  rankfilimbi  9909  r1filimi  9910  updjud  10022  tskwe  10038  infxpenlem  10099  fseqenlem1  10110  kmlem2  10237  nnadju  10283  cff1  10343  cflim2  10348  sornom  10362  infpssrlem4  10391  fin23lem26  10410  fin23lem30  10427  fin23lem34  10431  isf32lem11  10448  fin67  10480  isfin7-2  10481  fin1a2lem10  10494  axcc2lem  10521  axdc2lem  10533  axdc3lem2  10536  axdc3lem4  10538  axdc4lem  10540  iunfo  10630  tsk0  10855  gruina  10910  grur1a  10911  mulcanenq  11052  reclem2pr  11140  supsrlem  11203  supsr  11204  ax1rid  11253  negf1o  11753  lbreu  12274  nnindd  12362  nnaddcl  12365  nnmulcl  12366  nn0n0n1ge2b  12682  nn0indd  12803  fzind  12804  fnn0ind  12805  uzaddcl  13038  uzinfi  13062  nn01to3  13075  elpq  13110  xmulasslem2  13419  supxrunb1  13456  supxrunb2  13457  infmremnf  13481  infmrp1  13482  uzsubsubfz  13687  fzdif1  13746  elfz0ubfz0  13773  fz0fzdiffz0  13778  elfzmlbp  13780  fzofzim  13851  elfzom1elp1fzo  13874  ssfzo12bi  13903  fzoopth  13904  fzonfzoufzol  13913  elfznelfzob  13916  injresinjlem  13932  injresinj  13933  modaddmodup  14084  modfzo0difsn  14093  modsumfzodifsn  14094  addmodlteq  14096  om2uzlti  14100  fsequb  14125  ssnn0fi  14135  ser1const  14208  expcllem  14222  expeq0  14242  expmordi  14317  expnngt1  14392  faclbnd  14441  hashf1rn  14503  hashgadd  14528  hashunx  14537  hashnn0n0nn  14542  hashgt0elex  14552  hashss  14560  hashfzp1  14583  hashxp  14586  hashmap  14587  hashimarni  14593  seqcoll  14616  hash2exprb  14623  hashge2el2difr  14633  elss2prb  14640  hashdifsnp1  14658  fi1uzind  14659  brfi1indALT  14662  lswlgt0cl  14721  swrdnd  14812  swrdnnn0nd  14814  swrdnd0  14815  swrd0  14816  swrdsbslen  14822  swrdspsleq  14823  pfxsuff1eqwrdeq  14856  swrdswrdlem  14861  swrdswrd  14862  wrd2ind  14880  pfxccatin12lem2a  14884  swrdccatin2  14886  pfxccatin12lem2  14888  pfxccatin12lem3  14889  pfxccatin12  14890  pfxccat3  14891  swrdccat  14892  pfxccat3a  14895  swrdccat3blem  14896  repswswrd  14943  repswrevw  14946  cshwmodn  14954  cshwsublen  14955  cshwidxmod  14962  cshwidxmodr  14963  cshf1  14969  2cshw  14972  cshweqrep  14980  cshw1  14981  2cshwcshw  14984  cshwcshid  14986  cshwcsh2id  14987  wrdlen2i  15102  2swrd2eqwrdeq  15115  wwlktovfo  15120  relexpsucnnl  15192  rtrclreclem3  15222  rtrclreclem4  15223  relexpindlem  15225  r19.29uz  15527  caubnd  15535  sqreu  15537  climshft  15752  climub  15838  climserle  15839  sumss  15899  sumss2  15901  modfsummods  15969  o1fsum  15989  binom  16008  climcndslem1  16027  climcndslem2  16028  cvgrat  16061  clim2prod  16066  prodfn0  16072  prodfrec  16073  ntrivcvgfvn0  16077  fprodn0  16155  fprodmodd  16173  fprodefsum  16270  demoivreALT  16378  ruclem8  16414  dvdsaddre2b  16486  dvdsdivcl  16495  dvdsfac  16505  oddnn02np1  16527  oddge22np1  16528  evennn02n  16529  evennn2n  16530  m1exp1  16555  nn0o  16562  pwp1fsum  16570  flodddiv4  16594  smu01lem  16664  dvdslegcd  16683  gcdneg  16703  dfgcd2  16728  seq1st  16755  alginv  16759  lcmf  16817  lcmftp  16820  lcmfunsnlem2lem2  16823  lcmfunsnlem  16825  lcmfun  16829  ncoprmgcdne1b  16834  coprmproddvdslem  16846  coprmproddvds  16847  cncongr1  16851  prmdvdsexp  16900  prmndvdsfaclt  16910  ncoprmlnprm  16913  fvprmselgcd1  17232  prmgaplem6  17243  prmgaplem7  17244  prmgaplem8  17245  cshwshashlem1  17282  setsstruct2  17361  setsstruct  17363  inveq  17958  catsubcat  18023  initoeu2lem0  18197  initoeu2lem1  18198  funcestrcsetclem8  18330  funcestrcsetclem9  18331  fthestrcsetc  18333  fullestrcsetc  18334  funcsetcestrclem9  18346  fthsetcestrc  18348  fullsetcestrc  18349  lubss  18696  lubel  18697  mgmpropd  18838  issstrmgm  18840  mgmb1mgm1  18842  mgmidpfod  18866  frmdgsum  19067  smndex1mndlem  19117  mgm2nsgrplem3  19128  dfgrp2  19182  cyccom  19427  gaass  19520  gsumwrev  19589  symgextf1lem  19643  symgextf1  19644  fvcosymgeq  19652  gsmsymgreq  19655  symgfixelsi  19658  pmtrprfv3  19677  symggen  19693  pmtrprfval  19710  gsumzres  20132  gsumpr  20178  gsumzunsnd  20179  srgmulgass  20452  srgbinom  20466  0ringnnzr  20785  rnghmsscmap  20891  rnghmsubcsetclem2  20893  rngcinv  20898  funcrngcsetc  20901  funcrngcsetcALT  20902  rhmsscmap  20920  rhmsubcsetclem2  20922  rhmsubcrngclem2  20928  funcringcsetc  20935  srhmsubc  20941  rhmsubclem4  20949  lmodvsmmulgdi  21181  lmodfopnelem1  21182  rmodislmodlem  21213  rngqiprngimfo  21606  cnfldmulg  21719  cnfldexp  21720  ofldchr  21891  psgndiflemB  21915  assamulgscm  22218  gsumply1subr  22560  gsummoncoe1  22635  pf1ind  22682  matmulcell  22769  mat1dimscm  22799  dmatmul  22821  dmatscmcl  22827  scmataddcl  22840  scmatsubcl  22841  scmatsgrp1  22846  mavmulsolcl  22875  ma1repveval  22895  1marepvmarrepid  22899  symgmatr01lem  22977  matunitlindf  23005  slesolvec  23006  cramerimplem2  23011  decpmatmullem  23098  pm2mpf1  23126  mp2pm2mplem4  23136  monmat2matmon  23151  chpscmat  23169  chpscmatgsumbin  23171  fvmptnn04ifb  23178  chfacfscmul0  23185  chfacfscmulgsum  23187  chfacfpmmul0  23189  chfacfpmmulgsum  23191  cpmadugsumlemF  23203  toprntopon  23252  clsss  23381  ntrss  23382  restntr  23509  cmpsublem  23726  cmpsub  23727  2ndcrest  23781  txindislem  23961  t0kq  24146  filufint  24248  fbflim2  24305  flftg  24324  alexsubALTlem4  24378  cnextfvval  24393  ustuqtop4  24572  xmettri2  24668  mettri  24680  metss  24836  tngngp3  24984  clmvscom  25420  lmmbr  25588  caublcls  25639  lmcau  25643  ovolunlem1a  25826  nulmbl2  25866  voliunlem1  25880  iunmbl  25883  volsup  25886  dvlip  26322  dvfsumle  26350  degltlem1  26399  ply1divex  26464  plyco  26569  dgrnznn  26575  dvnply2  26617  plydivex  26627  aannenlem2  26665  aaliou3lem2  26679  ulmcau  26731  zabsle1  27632  gausslemma2dlem1a  27701  gausslemma2dlem2  27703  gausslemma2dlem3  27704  gausslemma2dlem4  27705  2lgslem1a1  27725  2sqnn0  27774  2sqreulem1  27782  2sqreunnlem1  27785  dchrisumlem1  27825  dchrisumlem2  27826  dchrisumlem3  27827  qabvle  27961  ostthlem2  27964  ostth2lem2  27970  nosupbnd1lem5  28078  noinfbnd1lem5  28093  nocvxminlem  28149  lesrec  28194  madebdaylemold  28293  mulsuniflem  28544  precsexlem6  28607  precsexlem7  28608  precsexlem8  28609  precsexlem9  28610  abssge0  28640  noseqind  28687  om2noseqlt  28694  om2noseqrdg  28699  n0addscl  28739  n0mulscl  28740  onsfi  28751  oldfib  28772  expscllem  28825  pw2cut2  28857  z12zsodd  28877  tgjustr  28945  axeuclidlem  29549  incistruhgr  29666  umgredgprv  29694  umgrpredgv  29727  usgredgprvALT  29785  uhgr2edg  29798  usgredg2vlem2  29816  lfuhgr1v0e  29844  subgrfun  29871  umgrres1lem  29900  upgrres1  29903  fusgrfis  29920  uhgrnbgr0nb  29944  nbgr1vtx  29948  nb3grprlem1  29970  uvtx01vtx  29987  fusgrn0degnn0  30089  vtxdginducedm1lem4  30132  finsumvtxdg2size  30140  wlkl1loop  30227  wlkres  30258  lfgrwlknloop  30281  pthdadjvtx  30322  dfpth2  30323  upgr2pthnlp  30327  upgrwlkdvdelem  30331  upgrwlkdvde  30332  uhgrwkspthlem2  30349  usgr2trlspth  30356  usgr2pth  30359  pthdlem2lem  30362  cyclnumvtx  30397  lfgrn1cycl  30403  uspgrn2crct  30406  crctcshwlkn0lem3  30410  crctcshwlkn0lem4  30411  crctcshwlkn0lem5  30412  iswspthsnon  30454  wlkiswwlks1  30465  wlklnwwlkln1  30466  wlkiswwlks2  30473  wlkiswwlksupgr2  30475  wlklnwwlkln2lem  30480  wlknwwlksnbij  30486  wwlksnred  30490  wwlksnext  30491  wwlksnredwwlkn  30493  wwlksnredwwlkn0  30494  wwlksnextfun  30496  wwlksnextinj  30497  wwlksnextsurj  30498  wspthsnonn0vne  30515  wspn0  30522  wwlks2onv  30551  elwwlks2  30567  elwspths2spth  30568  rusgrnumwwlk  30576  clwwlkccatlem  30589  clwlkclwwlklem2a1  30592  clwlkclwwlklem2fv2  30596  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlkf1lem3  30606  clwwisshclwwslem  30614  clwwisshclwwsn  30616  erclwwlktr  30622  isclwwlknx  30636  clwwlkinwwlk  30640  clwwlkel  30646  clwwlkf  30647  clwwlkf1  30649  clwwlkfo  30650  clwwlkext2edg  30656  wwlksext2clwwlk  30657  wwlksubclwwlk  30658  clwwlknscsh  30662  erclwwlkntr  30671  eleclclwwlkn  30676  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  clwwlknon0  30693  clwwlknonel  30695  clwwlknon1  30697  clwwlknonwwlknonb  30706  clwwlknonex2lem2  30708  clwwlknun  30712  clwwlkvbij  30713  upgr3v3e3cycl  30790  uhgr3cyclex  30792  upgr4cycl4dv4e  30795  eulerpath  30851  eucrctshift  30853  eucrct2eupth  30855  1to2vfriswmgr  30889  1to3vfriswmgr  30890  3cyclfrgrrn1  30895  4cycl2vnunb  30900  frgrwopreglem2  30923  frgrwopreglem3  30924  frgrwopreglem5ALT  30932  fusgr2wsp2nb  30944  2clwwlk2clwwlklem  30956  2clwwlk2clwwlk  30960  numclwwlk1lem2f1  30967  numclwwlk1lem2fo  30968  numclwwlk1  30971  clwwlknonclwlknonf1o  30972  dlwwlknondlwlknonf1o  30975  numclwlk1  30981  numclwlk2lem2f  30987  numclwlk2lem2f1o  30989  numclwwlk5  30998  frgrreg  31004  frgrregord013  31005  friendship  31009  nsnlplig  31092  nsnlpligALT  31093  isgrpo  31108  vcdi  31176  vcdir  31177  vcass  31178  nmosetre  31375  hlim2  31803  shscli  31928  chintcli  31942  dfch2  32018  spansncvi  32263  nmopsetretALT  32474  nmfnsetre  32488  lnopl  32525  lnfnl  32542  pjss2coi  32775  pjorthcoi  32780  pjscji  32781  pjssdif2i  32785  pjclem4a  32809  pj3lem1  32817  strlem5  32866  hstrlem5  32874  cvmdi  32935  mdslmd3i  32943  atcv1  32991  atcvat4i  33008  cdj3lem2a  33047  cdj3lem3a  33050  opreu2reuALT  33124  iuninc  33206  disji2f  33222  disjif2  33226  fmptcof2  33302  xrsmulgzz  33620  1arithufdlem3  34128  esumfzf  34751  issgon  34805  voliune  34912  volfiniune  34913  rrvsum  35136  bnj228  35416  bnj1294  35497  bnj229  35564  bnj607  35596  bnj908  35611  bnj953  35619  bnj1118  35664  bnj1174  35683  bnj1388  35713  trssfir1om  35793  trssfir1omregs  35864  prconf1acwevd  35971  acycgrsubgr  36003  cvmliftlem15  36153  satfsschain  36219  satfdm  36224  satf0op  36232  fmla0xp  36238  gonarlem  36249  goalrlem  36251  satffunlem1lem1  36257  satffunlem2lem1  36259  dmopab3rexdif  36260  satefvfmla0  36273  prv1n  36286  iprodefisumlem  36601  faclimlem1  36604  dfon2lem6  36646  idinside  36945  onsucconni  37321  axuntco  37363  ttcmin  37380  elttctr  37389  dfttc2g  37390  bj-cbvew  37637  axc11n11r  37681  bj-brrelex12ALT  38090  bj-snmoore  38142  bj-finsumval0  38315  exlimim  38374  exellim  38376  icoreclin  38389  difunieq  38406  fvineqsneq  38444  pibt2  38449  wl-spae  38562  wl-aleq  38576  fin2so  38639  poimirlem4  38651  poimirlem26  38673  itg2addnclem  38698  upixp  38772  welb  38779  sdclem2  38785  metf1o  38798  sstotbnd3  38819  isbndx  38825  ismtycnv  38845  heiborlem4  38857  bfplem1  38865  opidonOLD  38895  grpomndo  38918  eldisjdmqsim2  39857  ax12eq  40107  ax12el  40108  cvrat4  40609  nn0addcom  43635  nn0mulcom  43639  mzpexpmpt  43865  diophren  43929  rmxypos  44063  jm2.17a  44076  jm2.17b  44077  rmygeid  44080  jm2.18  44104  jm2.25  44115  jm2.15nn0  44119  jm2.16nn0  44120  pwslnm  44205  isnumbasgrplem1  44212  dgraalem  44256  onuniintrab  44337  onsupuni  44340  onsupcl3  44344  naddonnn  44506  naddwordnexlem2  44509  relexpiidm  44813  relexpmulnn  44818  relexpmulg  44819  relexp01min  44822  relexp0a  44825  relexpxpmin  44826  clsk1indlem3  45152  grucollcld  45353  dvgrat  45405  radcnvrat  45407  sspwimpcf  46010  sspwimpcfVD  46011  e2ebindALT  46019  trfr  46060  et-sqrtnegnre  47991  fsetprcnexALT  48240  aiotaexim  48276  eu2ndop1stv  48303  afvfv0bi  48330  afveu  48331  afvres  48350  aovmpt4g  48379  ndmaovass  48384  ndmaovdistr  48385  afv2orxorb  48406  afv2eu  48416  imarnf1pr  48460  nltle2tri  48491  fzopredsuc  48502  subsubelfzo0  48505  2ffzoeq  48506  2tceilhalfelfzo1  48514  m1modmmod  48542  smonoord  48555  elsetpreimafvssdm  48576  iccpartres  48608  iccpartiltu  48612  iccpartigtl  48613  iccpartgt  48617  icceuelpartlem  48625  fargshiftf1  48631  ichnreuop  48662  ichreuopeq  48663  elsprel  48665  sprsymrelfo  48687  prproropf1olem4  48696  paireqne  48701  sbcpr  48711  reupr  48712  goldbachth  48740  fmtnoprmfac1  48758  fmtnoprmfac2  48760  prmdvdsfmtnof1lem2  48778  lighneallem2  48799  lighneallem4  48803  requad2  48829  even3prm2  48925  fpprwpprb  48946  gbegt5  48967  sbgoldbwt  48983  sbgoldbm  48990  nnsum3primesgbe  48998  wtgoldbnnsum4prm  49008  bgoldbnnsum3prm  49010  bgoldbtbndlem2  49012  bgoldbtbndlem3  49013  bgoldbtbndlem4  49014  bgoldbtbnd  49015  isubgredg  49072  grimuhgr  49093  clnbgrgrim  49140  grtriprop  49147  cycl3grtrilem  49152  cycl3grtri  49153  gpgusgralem  49262  gpgedgvtx0  49267  gpgedgvtx1  49268  gpgcubic  49285  gpg5nbgr3star  49287  gpgprismgr4cycllem3  49303  upgrwlkupwlk  49346  uspgropssxp  49350  uspgrsprfo  49354  isassintop  49415  lidldomn1  49436  2zlidl  49445  2zrngamgm  49450  2zrngmmgm  49457  rngccatidALTV  49477  rngcinvALTV  49481  rhmsubcALTVlem4  49489  funcringcsetcALTV2lem9  49503  ringccatidALTV  49511  srhmsubcALTV  49530  lmodvsmdi  49599  ply1mulgsumlem1  49606  ply1mulgsumlem2  49607  lincdifsn  49644  lincsumcl  49651  lincscmcl  49652  lincext3  49676  lindslinindsimp1  49677  lindslinindsimp2lem5  49682  snlindsntor  49691  lincresunit2  49698  lincresunit3lem2  49700  zgtp1leeq  49741  elbigo2  49772  fllog2  49788  digexp  49827  dig1  49828  nn0sumshdiglemA  49839  nn0sumshdiglemB  49840  1arymaptf1  49862  2arymaptf1  49873  rrxlinec  49957  rrx2linest  49962  itsclc0yqsol  49984  itsclc0xyqsol  49988