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  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  3718  2reu1  3845  rexdifi  4097  r19.2z  4455  falseral0OLD  4471  elelpwi  4567  preqsnd  4819  prproe  4865  ssuni  4893  disji2  5087  disjiun  5091  disjxiun  5100  trintss  5231  ssexgOLD  5288  reusv2lem3  5365  propeqop  5484  otiunsndisj  5497  rexopabb  5506  pofun  5581  solin  5590  2optocl  5751  3optocl  5752  ssrelrn  5878  elrnmpt1  5944  resieq  5983  imadifssranOLD  6198  reuop  6291  fnun  6646  fss  6719  fun  6737  fvelimab  6950  fvmptss  6999  fvn0ssdmfun  7067  fvcofneq  7086  fmptco  7123  funsndifnop  7148  fnressn  7155  fressnfv  7157  fmptsng  7166  fvtp2g  7197  fvtp3g  7198  tpres  7200  fnex  7216  funfvima3  7235  fvf1pr  7308  isores3  7336  tfisg  7850  dmfex  7902  opreuopreu  8031  releldmdifi  8042  funeldmdif  8045  el2mpocsbcl  8082  f1o2ndf1  8119  frxp  8124  fnse  8131  frxp2  8142  frxp3  8149  poseq  8156  ressuppssdif  8183  funsssuppss  8188  mpoxopxnop0  8213  reldmtpos  8232  frrlem8  8292  fpr2a  8301  smores  8341  tfrlem7  8372  tz7.48-2  8431  tz7.49  8434  oacl  8522  omcl  8523  oecl  8524  oarec  8549  oewordri  8580  oeworde  8581  oelim2  8583  oeoa  8585  oeoelem  8586  oeoe  8587  nnacl  8599  nnmcl  8600  nnecl  8601  nnmsucr  8613  naddoa  8691  brinxper  8726  2ecoptocl  8808  fsetprcnex  8863  undifixp  8941  funen1cnv  9035  xpf1o  9137  limensuc  9152  unfi  9165  en1eqsn  9245  ac6sfi  9254  frfi  9255  difinf  9281  f1dmvrnfibi  9308  f1vrnfibi  9309  suppeqfsuppbi  9349  elfiun  9400  dffi3  9401  infsupprpr  9476  xpwdomg  9557  infdiffi  9637  ttrclselem2  9705  epfrs  9710  frmin  9731  frr2  9742  rankxpsuc  9864  updjud  9939  tskwe  9955  infxpenlem  10016  fseqenlem1  10027  kmlem2  10154  nnadju  10200  cff1  10260  cflim2  10265  sornom  10279  infpssrlem4  10308  fin23lem26  10327  fin23lem30  10344  fin23lem34  10348  isf32lem11  10365  fin67  10397  isfin7-2  10398  fin1a2lem10  10411  axcc2lem  10438  axdc2lem  10450  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  iunfo  10547  tsk0  10772  gruina  10827  grur1a  10828  mulcanenq  10969  reclem2pr  11057  supsrlem  11120  supsr  11121  ax1rid  11170  negf1o  11668  lbreu  12189  nnindd  12277  nnaddcl  12280  nnmulcl  12281  nn0n0n1ge2b  12597  nn0indd  12718  fzind  12719  fnn0ind  12720  uzaddcl  12953  uzinfi  12977  nn01to3  12990  elpq  13025  xmulasslem2  13334  supxrunb1  13371  supxrunb2  13372  infmremnf  13396  infmrp1  13397  uzsubsubfz  13601  fzdif1  13660  elfz0ubfz0  13687  fz0fzdiffz0  13692  elfzmlbp  13694  fzofzim  13765  elfzom1elp1fzo  13788  ssfzo12bi  13817  fzoopth  13818  fzonfzoufzol  13827  elfznelfzob  13830  injresinjlem  13846  injresinj  13847  modaddmodup  13998  modfzo0difsn  14007  modsumfzodifsn  14008  addmodlteq  14010  om2uzlti  14014  fsequb  14039  ssnn0fi  14049  ser1const  14122  expcllem  14136  expeq0  14156  expmordi  14231  expnngt1  14305  faclbnd  14354  hashf1rn  14416  hashgadd  14441  hashunx  14450  hashnn0n0nn  14455  hashgt0elex  14465  hashss  14473  hashfzp1  14496  hashxp  14499  hashmap  14500  hashimarni  14506  seqcoll  14529  hash2exprb  14536  hashge2el2difr  14546  elss2prb  14553  hashdifsnp1  14571  fi1uzind  14572  brfi1indALT  14575  lswlgt0cl  14634  swrdnd  14724  swrdnnn0nd  14726  swrdnd0  14727  swrd0  14728  swrdsbslen  14734  swrdspsleq  14735  pfxsuff1eqwrdeq  14768  swrdswrdlem  14773  swrdswrd  14774  wrd2ind  14792  pfxccatin12lem2a  14796  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccatin12lem3  14801  pfxccatin12  14802  pfxccat3  14803  swrdccat  14804  pfxccat3a  14807  swrdccat3blem  14808  repswswrd  14855  repswrevw  14858  cshwmodn  14866  cshwsublen  14867  cshwidxmod  14874  cshwidxmodr  14875  cshf1  14881  2cshw  14884  cshweqrep  14892  cshw1  14893  2cshwcshw  14896  cshwcshid  14898  cshwcsh2id  14899  wrdlen2i  15013  2swrd2eqwrdeq  15026  wwlktovfo  15031  relexpsucnnl  15103  rtrclreclem3  15133  rtrclreclem4  15134  relexpindlem  15136  r19.29uz  15438  caubnd  15446  sqreu  15448  climshft  15663  climub  15749  climserle  15750  sumss  15810  sumss2  15812  modfsummods  15880  o1fsum  15900  binom  15919  climcndslem1  15938  climcndslem2  15939  cvgrat  15972  clim2prod  15977  prodfn0  15983  prodfrec  15984  ntrivcvgfvn0  15988  fprodn0  16066  fprodmodd  16084  fprodefsum  16181  demoivreALT  16289  ruclem8  16325  dvdsaddre2b  16397  dvdsdivcl  16406  dvdsfac  16416  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  m1exp1  16466  nn0o  16473  pwp1fsum  16481  flodddiv4  16505  smu01lem  16575  dvdslegcd  16594  gcdneg  16612  dfgcd2  16636  seq1st  16661  alginv  16665  lcmf  16723  lcmftp  16726  lcmfunsnlem2lem2  16729  lcmfunsnlem  16731  lcmfun  16735  ncoprmgcdne1b  16740  coprmproddvdslem  16752  coprmproddvds  16753  cncongr1  16757  prmdvdsexp  16806  prmndvdsfaclt  16816  ncoprmlnprm  16819  fvprmselgcd1  17137  prmgaplem6  17148  prmgaplem7  17149  prmgaplem8  17150  cshwshashlem1  17187  setsstruct2  17266  setsstruct  17268  inveq  17863  catsubcat  17928  initoeu2lem0  18102  initoeu2lem1  18103  funcestrcsetclem8  18235  funcestrcsetclem9  18236  fthestrcsetc  18238  fullestrcsetc  18239  funcsetcestrclem9  18251  fthsetcestrc  18253  fullsetcestrc  18254  lubss  18601  lubel  18602  mgmpropd  18743  issstrmgm  18745  mgmb1mgm1  18747  mgmidpfod  18770  sgrpidmnd  18841  frmdgsum  18971  smndex1mndlem  19021  mgm2nsgrplem3  19032  dfgrp2  19086  cyccom  19331  gaass  19424  gsumwrev  19493  symgextf1lem  19547  symgextf1  19548  fvcosymgeq  19556  gsmsymgreq  19559  symgfixelsi  19562  pmtrprfv3  19581  symggen  19597  pmtrprfval  19614  gsumzres  20036  gsumpr  20082  gsumzunsnd  20083  srgmulgass  20356  srgbinom  20370  0ringnnzr  20686  rnghmsscmap  20792  rnghmsubcsetclem2  20794  rngcinv  20799  funcrngcsetc  20802  funcrngcsetcALT  20803  rhmsscmap  20821  rhmsubcsetclem2  20823  rhmsubcrngclem2  20829  funcringcsetc  20836  srhmsubc  20842  rhmsubclem4  20850  lmodvsmmulgdi  21081  lmodfopnelem1  21082  rmodislmodlem  21113  rngqiprngimfo  21504  cnfldmulg  21617  cnfldexp  21618  ofldchr  21789  psgndiflemB  21813  assamulgscm  22116  gsumply1subr  22458  gsummoncoe1  22533  pf1ind  22580  matmulcell  22667  mat1dimscm  22697  dmatmul  22719  dmatscmcl  22725  scmataddcl  22738  scmatsubcl  22739  scmatsgrp1  22744  mavmulsolcl  22773  ma1repveval  22793  1marepvmarrepid  22797  symgmatr01lem  22875  matunitlindf  22903  slesolvec  22904  cramerimplem2  22909  decpmatmullem  22996  pm2mpf1  23024  mp2pm2mplem4  23034  monmat2matmon  23049  chpscmat  23067  chpscmatgsumbin  23069  fvmptnn04ifb  23076  chfacfscmul0  23083  chfacfscmulgsum  23085  chfacfpmmul0  23087  chfacfpmmulgsum  23089  cpmadugsumlemF  23101  toprntopon  23150  clsss  23279  ntrss  23280  restntr  23407  cmpsublem  23624  cmpsub  23625  2ndcrest  23679  txindislem  23859  t0kq  24044  filufint  24146  fbflim2  24203  flftg  24222  alexsubALTlem4  24276  cnextfvval  24291  ustuqtop4  24470  xmettri2  24566  mettri  24578  metss  24734  tngngp3  24882  clmvscom  25318  lmmbr  25486  caublcls  25537  lmcau  25541  ovolunlem1a  25724  nulmbl2  25764  voliunlem1  25778  iunmbl  25781  volsup  25784  dvlip  26220  dvfsumle  26248  degltlem1  26297  ply1divex  26362  plyco  26467  dgrnznn  26473  dvnply2  26517  plydivex  26527  aannenlem2  26565  aaliou3lem2  26579  ulmcau  26631  zabsle1  27532  gausslemma2dlem1a  27601  gausslemma2dlem2  27603  gausslemma2dlem3  27604  gausslemma2dlem4  27605  2lgslem1a1  27625  2sqnn0  27674  2sqreulem1  27682  2sqreunnlem1  27685  dchrisumlem1  27725  dchrisumlem2  27726  dchrisumlem3  27727  qabvle  27861  ostthlem2  27864  ostth2lem2  27870  nosupbnd1lem5  27948  noinfbnd1lem5  27963  nocvxminlem  28019  lesrec  28064  madebdaylemold  28163  mulsuniflem  28414  precsexlem6  28477  precsexlem7  28478  precsexlem8  28479  precsexlem9  28480  abssge0  28510  noseqind  28557  om2noseqlt  28564  om2noseqrdg  28569  n0addscl  28609  n0mulscl  28610  onsfi  28621  oldfib  28642  expscllem  28695  pw2cut2  28727  z12zsodd  28747  tgjustr  28815  axeuclidlem  29419  incistruhgr  29536  umgredgprv  29564  umgrpredgv  29597  usgredgprvALT  29655  uhgr2edg  29668  usgredg2vlem2  29686  lfuhgr1v0e  29714  subgrfun  29741  umgrres1lem  29770  upgrres1  29773  fusgrfis  29790  uhgrnbgr0nb  29814  nbgr1vtx  29818  nb3grprlem1  29840  uvtx01vtx  29857  fusgrn0degnn0  29959  vtxdginducedm1lem4  30002  finsumvtxdg2size  30010  wlkl1loop  30097  wlkres  30128  lfgrwlknloop  30151  pthdadjvtx  30192  dfpth2  30193  upgr2pthnlp  30197  upgrwlkdvdelem  30201  upgrwlkdvde  30202  uhgrwkspthlem2  30219  usgr2trlspth  30226  usgr2pth  30229  pthdlem2lem  30232  cyclnumvtx  30267  lfgrn1cycl  30273  uspgrn2crct  30276  crctcshwlkn0lem3  30280  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  iswspthsnon  30324  wlkiswwlks1  30335  wlklnwwlkln1  30336  wlkiswwlks2  30343  wlkiswwlksupgr2  30345  wlklnwwlkln2lem  30350  wlknwwlksnbij  30356  wwlksnred  30360  wwlksnext  30361  wwlksnredwwlkn  30363  wwlksnredwwlkn0  30364  wwlksnextfun  30366  wwlksnextinj  30367  wwlksnextsurj  30368  wspthsnonn0vne  30385  wspn0  30392  wwlks2onv  30421  elwwlks2  30437  elwspths2spth  30438  rusgrnumwwlk  30446  clwwlkccatlem  30459  clwlkclwwlklem2a1  30462  clwlkclwwlklem2fv2  30466  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlklem2  30470  clwlkclwwlkf1lem3  30476  clwwisshclwwslem  30484  clwwisshclwwsn  30486  erclwwlktr  30492  isclwwlknx  30506  clwwlkinwwlk  30510  clwwlkel  30516  clwwlkf  30517  clwwlkf1  30519  clwwlkfo  30520  clwwlkext2edg  30526  wwlksext2clwwlk  30527  wwlksubclwwlk  30528  clwwlknscsh  30532  erclwwlkntr  30541  eleclclwwlkn  30546  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  clwwlknon0  30563  clwwlknonel  30565  clwwlknon1  30567  clwwlknonwwlknonb  30576  clwwlknonex2lem2  30578  clwwlknun  30582  clwwlkvbij  30583  upgr3v3e3cycl  30660  uhgr3cyclex  30662  upgr4cycl4dv4e  30665  eulerpath  30721  eucrctshift  30723  eucrct2eupth  30725  1to2vfriswmgr  30759  1to3vfriswmgr  30760  3cyclfrgrrn1  30765  4cycl2vnunb  30770  frgrwopreglem2  30793  frgrwopreglem3  30794  frgrwopreglem5ALT  30802  fusgr2wsp2nb  30814  2clwwlk2clwwlklem  30826  2clwwlk2clwwlk  30830  numclwwlk1lem2f1  30837  numclwwlk1lem2fo  30838  numclwwlk1  30841  clwwlknonclwlknonf1o  30842  dlwwlknondlwlknonf1o  30845  numclwlk1  30851  numclwlk2lem2f  30857  numclwlk2lem2f1o  30859  numclwwlk5  30868  frgrreg  30874  frgrregord013  30875  friendship  30879  nsnlplig  30962  nsnlpligALT  30963  isgrpo  30978  vcdi  31046  vcdir  31047  vcass  31048  nmosetre  31245  hlim2  31673  shscli  31798  chintcli  31812  dfch2  31888  spansncvi  32133  nmopsetretALT  32344  nmfnsetre  32358  lnopl  32395  lnfnl  32412  pjss2coi  32645  pjorthcoi  32650  pjscji  32651  pjssdif2i  32655  pjclem4a  32679  pj3lem1  32687  strlem5  32736  hstrlem5  32744  cvmdi  32805  mdslmd3i  32813  atcv1  32861  atcvat4i  32878  cdj3lem2a  32917  cdj3lem3a  32920  opreu2reuALT  32952  iuninc  33034  disji2f  33050  disjif2  33054  fmptcof2  33130  xrsmulgzz  33449  1arithufdlem3  33956  esumfzf  34579  issgon  34633  voliune  34740  volfiniune  34741  rrvsum  34965  bnj228  35245  bnj1294  35326  bnj229  35393  bnj607  35425  bnj908  35440  bnj953  35448  bnj1118  35493  bnj1174  35512  bnj1388  35542  rankfilimbi  35609  r1filimi  35611  trssfir1om  35621  trssfir1omregs  35662  acycgrsubgr  35737  cvmliftlem15  35877  satfsschain  35943  satfdm  35948  satf0op  35956  fmla0xp  35962  gonarlem  35973  goalrlem  35975  satffunlem1lem1  35981  satffunlem2lem1  35983  dmopab3rexdif  35984  satefvfmla0  35997  prv1n  36010  iprodefisumlem  36319  faclimlem1  36322  dfon2lem6  36365  idinside  36664  onsucconni  37056  axuntco  37098  ttcmin  37115  elttctr  37124  dfttc2g  37125  mh-inf3f1  37160  bj-cbvew  37372  axc11n11r  37416  bj-brrelex12ALT  37811  bj-snmoore  37863  bj-finsumval0  38037  exlimim  38096  exellim  38098  icoreclin  38111  difunieq  38128  fvineqsneq  38166  pibt2  38171  wl-spae  38284  wl-aleq  38298  fin2so  38361  poimirlem4  38373  poimirlem26  38395  itg2addnclem  38420  upixp  38479  welb  38486  sdclem2  38492  metf1o  38505  sstotbnd3  38526  isbndx  38532  ismtycnv  38552  heiborlem4  38564  bfplem1  38572  opidonOLD  38602  grpomndo  38625  eldisjdmqsim2  39564  ax12eq  39814  ax12el  39815  cvrat4  40316  nn0addcom  43350  nn0mulcom  43354  mzpexpmpt  43590  diophren  43654  rmxypos  43788  jm2.17a  43801  jm2.17b  43802  rmygeid  43805  jm2.18  43829  jm2.25  43840  jm2.15nn0  43844  jm2.16nn0  43845  pwslnm  43935  isnumbasgrplem1  43942  dgraalem  43986  onuniintrab  44067  onsupuni  44070  onsupcl3  44074  naddonnn  44236  naddwordnexlem2  44239  relexpiidm  44544  relexpmulnn  44549  relexpmulg  44550  relexp01min  44553  relexp0a  44556  relexpxpmin  44557  clsk1indlem3  44883  grucollcld  45084  dvgrat  45136  radcnvrat  45138  sspwimpcf  45742  sspwimpcfVD  45743  e2ebindALT  45751  trfr  45785  et-sqrtnegnre  47701  fsetprcnexALT  47950  eu2ndop1stv  48013  afvfv0bi  48040  afveu  48041  afvres  48060  aovmpt4g  48089  ndmaovass  48094  ndmaovdistr  48095  afv2orxorb  48116  afv2eu  48126  imarnf1pr  48170  nltle2tri  48201  fzopredsuc  48212  subsubelfzo0  48215  2ffzoeq  48216  2tceilhalfelfzo1  48224  m1modmmod  48252  smonoord  48265  elsetpreimafvssdm  48286  iccpartres  48318  iccpartiltu  48322  iccpartigtl  48323  iccpartgt  48327  icceuelpartlem  48335  fargshiftf1  48341  ichnreuop  48372  ichreuopeq  48373  elsprel  48375  sprsymrelfo  48397  prproropf1olem4  48406  paireqne  48411  sbcpr  48421  reupr  48422  goldbachth  48450  fmtnoprmfac1  48468  fmtnoprmfac2  48470  prmdvdsfmtnof1lem2  48488  lighneallem2  48509  lighneallem4  48513  requad2  48539  even3prm2  48635  fpprwpprb  48656  gbegt5  48677  sbgoldbwt  48693  sbgoldbm  48700  nnsum3primesgbe  48708  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  bgoldbtbndlem4  48724  bgoldbtbnd  48725  isubgredg  48782  grimuhgr  48803  clnbgrgrim  48850  grtriprop  48857  cycl3grtrilem  48862  cycl3grtri  48863  gpgusgralem  48972  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgcubic  48995  gpg5nbgr3star  48997  gpgprismgr4cycllem3  49013  upgrwlkupwlk  49056  uspgropssxp  49060  uspgrsprfo  49064  isassintop  49125  lidldomn1  49146  2zlidl  49155  2zrngamgm  49160  2zrngmmgm  49167  rngccatidALTV  49187  rngcinvALTV  49191  rhmsubcALTVlem4  49199  funcringcsetcALTV2lem9  49213  ringccatidALTV  49221  srhmsubcALTV  49240  lmodvsmdi  49309  ply1mulgsumlem1  49316  ply1mulgsumlem2  49317  lincdifsn  49354  lincsumcl  49361  lincscmcl  49362  lincext3  49386  lindslinindsimp1  49387  lindslinindsimp2lem5  49392  snlindsntor  49401  lincresunit2  49408  lincresunit3lem2  49410  zgtp1leeq  49451  elbigo2  49482  fllog2  49498  digexp  49537  dig1  49538  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  1arymaptf1  49572  2arymaptf1  49583  rrxlinec  49666  eenglngeehlnm  49669  rrx2linest  49672  itsclc0yqsol  49694  itsclc0xyqsol  49698