Theorem impcom 446

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  mpan9  486  bianir  1009  19.29r  1802  19.41v  1914  equtr2OLD  1956  equvinvOLD  1962  19.41  2103  nfsb4t  2389  2euex  2544  gencl  3235  2gencl  3236  vtocl4g  3277  rspccva  3308  sseq0  3975  minelOLD  4034  r19.2z  4060  falseral0  4081  elelpwi  4171  eqoreldifOLD  4226  prproe  4434  ssuni  4459  ssuniOLD  4460  disji2  4636  invdisjrab  4639  disjiun  4640  disjxiun  4649  trintss  4769  ssexg  4804  reusv2lem3  4871  propeqop  4970  otiunsndisj  4980  pofun  5051  solin  5058  2optocl  5196  3optocl  5197  ssrelrn  5315  elrnmpt1  5374  resieq  5407  funimaexg  5975  fnun  5997  fss  6056  fun  6066  fvelimab  6253  fvmptss  6292  fvn0ssdmfun  6350  fvcofneq  6367  fmptco  6396  funsndifnop  6416  fnressn  6425  fressnfv  6427  fvn0fvelrn  6430  fmptsng  6434  fvtp2g  6464  fvtp3g  6465  tpres  6466  fnex  6481  funfvima3  6495  isores3  6585  dmfex  7124  el2mpt2csbcl  7250  f1o2ndf1  7285  frxp  7287  fnse  7294  ressuppssdif  7316  funsssuppss  7321  suppss  7325  mpt2xopxnop0  7341  reldmtpos  7360  wfrfun  7425  wfrlem12  7426  smores  7449  tfrlem7  7479  tz7.48-2  7537  tz7.49  7540  oacl  7615  omcl  7616  oecl  7617  oarec  7642  oewordri  7672  oeworde  7673  oelim2  7675  oeoa  7677  oeoelem  7678  oeoe  7679  nnacl  7691  nnmcl  7692  nnecl  7693  nnmsucr  7705  2ecoptocl  7838  undifixp  7944  ssct  8041  xpf1o  8122  limensuc  8137  ac6sfi  8204  frfi  8205  difinf  8230  f1dmvrnfibi  8250  f1vrnfibi  8251  suppeqfsuppbi  8289  elfiun  8336  dffi3  8337  xpwdomg  8490  preleq  8514  infdiffi  8555  epfrs  8607  rankxpsuc  8745  tskwe  8776  infxpenlem  8836  fseqenlem1  8847  kmlem2  8973  cff1  9080  cflim2  9085  sornom  9099  infpssrlem4  9128  fin23lem26  9147  fin23lem30  9164  fin23lem34  9168  isf32lem11  9185  fin67  9217  isfin7-2  9218  fin1a2lem10  9231  axcc2lem  9258  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  iunfo  9361  tsk0  9585  gruina  9640  grur1a  9641  mulcanenq  9782  reclem2pr  9870  supsrlem  9932  supsr  9933  ax1rid  9982  negf1o  10460  mulgt1  10882  fiminre  10972  lbreu  10973  nnaddcl  11042  nnmulcl  11043  nn0n0n1ge2b  11359  nn0indd  11474  fzind  11475  fnn0ind  11476  uzaddcl  11744  uzinfi  11768  nn01to3  11781  xmulasslem2  12112  supxrunb1  12149  supxrunb2  12150  infmremnf  12173  infmrp1  12174  uzsubsubfz  12363  elfz0ubfz0  12443  fz0fzdiffz0  12448  elfzmlbp  12450  fzofzim  12514  elfzom1elp1fzo  12534  elfzom1p1elfzo  12547  ssfzo12bi  12563  fzonfzoufzol  12571  elfznelfzob  12574  injresinjlem  12588  injresinj  12589  modaddmodup  12733  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  om2uzlti  12749  fsequb  12774  ssnn0fi  12784  ser1const  12857  expcllem  12871  expeq0  12890  faclbnd  13077  faclbnd6  13086  hasheqf1oiOLD  13141  hashf1rn  13142  hashf1rnOLD  13143  hashgadd  13166  hashunx  13175  hashnn0n0nn  13180  hashgt0elex  13189  hashss  13197  hashfzp1  13218  hashxp  13221  hashimarni  13228  seqcoll  13248  hash2exprb  13253  hashge2el2difr  13263  elss2prb  13269  brfi1indlem  13278  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  lswlgt0cl  13356  swrdnd  13432  swrd0  13434  swrdsbslen  13448  swrdspsleq  13449  2swrd1eqwrdeq  13454  swrdswrdlem  13459  swrdswrd  13460  wrd2ind  13477  swrdccatfn  13482  swrdccatin1  13483  swrdccatin12lem2a  13485  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccatin12  13491  swrdccat3  13492  swrdccat  13493  swrdccat3blem  13495  repswswrd  13531  repswrevw  13533  cshwmodn  13541  cshwsublen  13542  cshwidxmod  13549  cshwidxmodr  13550  cshf1  13556  2cshw  13559  cshweqrep  13567  cshw1  13568  2cshwcshw  13571  cshwcshid  13573  cshwcsh2id  13574  wrdlen2i  13686  2swrd2eqwrdeq  13696  wwlktovfo  13701  relexpsucnnl  13772  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  cjexp  13890  absexp  14044  r19.29uz  14090  caubnd  14098  sqreu  14100  climshft  14307  climub  14392  climserle  14393  sumss  14455  sumss2  14457  modfsummods  14525  o1fsum  14545  binom  14562  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  pwm1geoser  14600  cvgrat  14615  clim2prod  14620  prodfn0  14626  prodfrec  14627  ntrivcvgfvn0  14631  fprodn0  14709  fprodmodd  14728  fprodefsum  14825  demoivreALT  14931  znnenlem  14940  ruclem8  14966  dvdsaddre2b  15029  dvdsdivcl  15038  dvdsfac  15048  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  m1exp1  15093  nn0o  15099  pwp1fsum  15114  flodddiv4  15137  smu01lem  15207  dvdslegcd  15226  gcdneg  15243  dfgcd2  15263  gcdmultiple  15269  seq1st  15284  alginv  15288  lcmf  15346  lcmftp  15349  lcmfunsnlem2lem2  15352  lcmfunsnlem  15354  lcmfun  15358  ncoprmgcdne1b  15363  coprmproddvdslem  15376  coprmproddvds  15377  cncongr1  15381  prmdvdsexp  15427  prmndvdsfaclt  15435  ncoprmlnprm  15436  fvprmselgcd1  15749  prmgaplem6  15760  prmgaplem7  15761  prmgaplem8  15762  cshwshashlem1  15802  setsstruct2  15896  setsstruct  15898  inveq  16434  catsubcat  16499  initoeu2lem0  16663  initoeu2lem1  16664  funcestrcsetclem8  16787  funcestrcsetclem9  16788  fthestrcsetc  16790  fullestrcsetc  16791  funcsetcestrclem9  16803  fthsetcestrc  16805  fullsetcestrc  16806  lubss  17121  lubel  17122  issstrmgm  17252  mgmb1mgm1  17254  frmdgsum  17399  mgm2nsgrplem3  17407  dfgrp2  17447  gaass  17730  gsumwrev  17796  symgextf1lem  17840  symgextf1  17841  fvcosymgeq  17849  gsmsymgreq  17852  symgfixelsi  17855  pmtrprfv3  17874  symggen  17890  pmtrprfval  17907  gsumzres  18310  gsumzunsnd  18355  srgmulgass  18531  srgbinom  18545  lmodvsmmulgdi  18898  lmodfopnelem1  18899  rmodislmodlem  18930  0ringnnzr  19269  assamulgscm  19350  gsumply1subr  19604  gsummoncoe1  19674  pf1ind  19719  cnfldmulg  19778  cnfldexp  19779  psgndiflemB  19946  matmulcell  20251  mat1dimscm  20281  dmatmul  20303  dmatscmcl  20309  scmataddcl  20322  scmatsubcl  20323  scmatsgrp1  20328  mavmulsolcl  20357  ma1repveval  20377  1marepvmarrepid  20381  symgmatr01lem  20459  slesolvec  20485  cramerimplem2  20490  decpmatmullem  20576  pm2mpf1  20604  mp2pm2mplem4  20614  monmat2matmon  20629  chpscmat  20647  chpscmatgsumbin  20649  fvmptnn04ifb  20656  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  cpmadugsumlemF  20681  clsss  20858  ntrss  20859  restntr  20986  cmpsublem  21202  cmpsub  21203  2ndcrest  21257  txindislem  21436  t0kq  21621  filufint  21724  fbflim2  21781  flftg  21800  alexsubALTlem4  21854  cnextfvval  21869  tmdmulg  21896  ustuqtop4  22048  xmettri2  22145  mettri  22157  metss  22313  tngngp3  22460  clmvscom  22890  lmmbr  23056  caublcls  23107  lmcau  23111  ovolunlem1a  23264  nulmbl2  23304  voliunlem1  23318  iunmbl  23321  volsup  23324  dvlip  23756  dvfsumle  23784  degltlem1  23832  ply1divex  23896  plyco  23997  dgrnznn  24003  dvnply2  24042  plydivex  24052  aannenlem2  24084  aaliou3lem2  24098  ulmcau  24149  zabsle1  25021  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  gausslemma2dlem4  25094  2lgslem1a1  25114  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  qabvle  25314  ostthlem2  25317  ostth2lem2  25323  axeuclidlem  25842  incistruhgr  25974  umgredgprv  26002  umgrpredgv  26035  usgredgprvALT  26087  uhgr2edg  26100  usgredg2vlem2  26118  lfuhgr1v0e  26146  subgrfun  26173  umgrres1lem  26202  upgrres1  26205  fusgrfis  26222  uhgrnbgr0nb  26250  nbgr1vtx  26254  nb3grprlem1  26282  uvtxa01vtx0  26297  uvtx2vtx1edg  26299  fusgrn0degnn0  26395  vtxdginducedm1lem4  26438  finsumvtxdg2size  26446  upgrewlkle2  26502  wlkl1loop  26534  wlkres  26567  lfgrwlknloop  26586  pthdadjvtx  26626  upgr2pthnlp  26628  upgrwlkdvdelem  26632  upgrwlkdvde  26633  uhgrwkspthlem2  26650  usgr2trlspth  26657  usgr2pth  26660  pthdlem2lem  26663  lfgrn1cycl  26697  uspgrn2crct  26700  crctcshwlkn0lem3  26704  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wspthnonp  26744  wlkiswwlks1  26753  wlklnwwlkln1  26754  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnext  26788  wwlksnredwwlkn  26790  wwlksnredwwlkn0  26791  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextsur  26795  wspthsnonn0vne  26813  wspn0  26820  wwlks2onv  26847  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlk  26870  clwwlknclwwlkdifs  26873  isclwwlksnx  26889  clwlkclwwlklem2a1  26893  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlkinwwlk  26905  clwwlksel  26914  clwwlksf  26915  clwwlksf1  26917  clwwlksfo  26918  clwwlksnwwlkncl  26921  clwwlksvbij  26922  clwwlksext2edg  26923  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwwisshclwwslem  26927  clwwisshclwwsn  26929  erclwwlkstr  26936  clwwlksnscsh  26940  erclwwlksntr  26948  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  clwlksfoclwwlk  26963  clwwlksnun  26974  upgr3v3e3cycl  27040  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  eulerpath  27101  eucrctshift  27103  eucrct2eupth  27105  1to2vfriswmgr  27143  1to3vfriswmgr  27144  3cyclfrgrrn1  27149  4cycl2vnunb  27154  frgrwopreglem2  27177  frgrwopreglem3  27178  frgrwopreglem5ALT  27186  fusgr2wsp2nb  27198  clwwlkextfrlem1  27208  numclwwlkovf2exlem2  27212  numclwlk1lem2foa  27224  numclwlk1lem2f1  27227  numclwlk1lem2fo  27228  numclwwlk1  27231  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  numclwwlk5  27246  frgrreg  27252  frgrregord013  27253  friendship  27257  nsnlplig  27333  nsnlpligALT  27334  isgrpo  27351  vcdi  27420  vcdir  27421  vcass  27422  nmosetre  27619  hlim2  28049  shscli  28176  chintcli  28190  dfch2  28266  spansncvi  28511  nmopsetretALT  28722  nmfnsetre  28736  lnopl  28773  lnfnl  28790  pjss2coi  29023  pjorthcoi  29028  pjscji  29029  pjssdif2i  29033  pjclem4a  29057  pj3lem1  29065  strlem5  29114  hstrlem5  29122  cvmdi  29183  mdslmd3i  29191  atcv1  29239  atcvat4i  29256  cdj3lem2a  29295  cdj3lem3a  29298  iuninc  29379  disji2f  29390  disjif2  29394  fmptcof2  29457  nnindd  29566  xrsmulgzz  29678  ofldchr  29814  esumfzf  30131  issgon  30186  voliune  30292  volfiniune  30293  rrvsum  30516  bnj228  30803  bnj1294  30888  bnj229  30954  bnj607  30986  bnj908  31001  bnj953  31009  bnj1118  31052  bnj1174  31071  bnj1388  31101  cvmliftlem15  31280  iprodefisumlem  31626  faclimlem1  31629  dfon2lem6  31693  tfisg  31716  poseq  31750  frrlem4  31783  frrlem5c  31786  frrlem11  31792  noprefixmo  31848  nosupbnd1lem5  31858  nocvxminlem  31893  nocvxmin  31894  slerec  31923  idinside  32191  nn0prpw  32318  onsucconni  32436  axc11n11r  32673  bj-finsumval0  33147  exlimim  33189  exellim  33192  icoreclin  33205  wl-spae  33306  wl-aleq  33322  fin2so  33396  matunitlindf  33407  poimirlem4  33413  poimirlem26  33435  itg2addnclem  33461  upixp  33524  welb  33531  sdclem2  33538  metf1o  33551  sstotbnd3  33575  isbndx  33581  ismtycnv  33601  heiborlem4  33613  bfplem1  33621  opidonOLD  33651  grpomndo  33674  ax12eq  34226  ax12el  34227  cvrat4  34729  mzpexpmpt  37308  diophren  37377  expmordi  37512  rmxypos  37514  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.18  37555  jm2.25  37566  jm2.15nn0  37570  jm2.16nn0  37571  pwslnm  37664  isnumbasgrplem1  37671  dgraalem  37715  relexpiidm  37996  relexpmulnn  38001  relexpmulg  38002  relexp01min  38005  relexp0a  38008  relexpxpmin  38009  clsk1indlem3  38341  dvgrat  38511  radcnvrat  38513  sspwimpcf  39156  sspwimpcfVD  39157  e2ebindALT  39165  2reurex  41181  2reu1  41186  eu2ndop1stv  41202  afvfv0bi  41232  afveu  41233  afvres  41252  aovmpt4g  41281  ndmaovass  41286  ndmaovdistr  41287  imarnf1pr  41301  nltle2tri  41323  fzopredsuc  41333  subsubelfzo0  41336  fzoopth  41337  2ffzoeq  41338  smonoord  41341  iccpartres  41354  iccpartiltu  41358  iccpartigtl  41359  iccpartgt  41363  icceuelpartlem  41371  fargshiftf1  41377  pfxsuff1eqwrdeq  41407  pfxccatin12lem2  41424  pfxccatin12  41425  pfxccat3  41426  pfxccat3a  41429  cshword2  41437  goldbachth  41459  fmtnoprmfac1  41477  fmtnoprmfac2  41479  prmdvdsfmtnof1lem2  41497  lighneallem2  41523  lighneallem4  41527  even3prm2  41628  gbegt5  41649  sbgoldbwt  41665  sbgoldbm  41672  nnsum3primesgbe  41680  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  upgrwlkupwlk  41721  elsprel  41725  sprsymrelfo  41747  uspgropssxp  41752  uspgrsprfo  41756  mgmpropd  41775  isassintop  41846  lidldomn1  41921  lidlmmgm  41925  2zlidl  41934  2zrngamgm  41939  2zrngmmgm  41946  rnghmsscmap  41974  rnghmsubcsetclem2  41976  rngcinv  41981  rngccatidALTV  41989  rngcinvALTV  41993  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap  42020  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  ringcinv  42032  funcringcsetc  42035  funcringcsetcALTV2lem9  42044  ringccatidALTV  42052  ringcinvALTV  42056  srhmsubc  42076  rhmsubclem4  42089  srhmsubcALTV  42094  rhmsubcALTVlem4  42107  gsumpr  42139  lmodvsmdi  42163  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  lincdifsn  42213  lincsumcl  42220  lincscmcl  42221  lincext3  42245  lindslinindsimp1  42246  lindslinindsimp2lem5  42251  snlindsntor  42260  lincresunit2  42267  lincresunit3lem2  42269  lincresunit3  42270  zgtp1leeq  42311  m1modmmod  42316  elbigo2  42346  fllog2  42362  digexp  42401  dig1  42402  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414