Theorem expcom 419

Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
ex.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
expcom	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		ex.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 33	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:  ancoms  464  pm3.21  477  sylan  592  animpimp2impd  860  4casesdan  1057  dedlema  1061  dedlemb  1062  sbiedvw  2133  mo4  2596  2moswapv  2659  2moswap  2674  2eu2  2682  pm2.61ne  3045  nelelne  3061  r19.21be  3260  rspcebdv  3577  2reu2  3853  csbie2df  4408  minel  4426  uneqdifeq  4455  raltpd  4749  ssunsn2  4795  opthprneg  4832  ssuni  4900  uniss2  4909  elpwuni  5073  intss2  5076  disjord  5100  elpw2g  5306  elssabg  5315  axprlem3OLD  5402  axprlem4OLD  5403  axprlem5OLD  5404  axprglem  5409  oteqex  5485  otsndisj  5504  otiunsndisj  5505  epelg  5564  wereu  5659  relop  5838  riinint  5964  sotri3  6132  unixpid  6289  reuop  6298  ordtr2  6410  ordsssuc2  6458  iotan0  6530  funopg  6574  fun  6744  fvmptnf  7016  fvn0ssdmfun  7073  eldmrexrnb  7091  fmptco  7129  fnressn  7159  fressnfv  7161  fprb  7196  fvtp2g  7201  fvtp3g  7202  fconst2g  7205  fntpb  7211  f1dom3el3dif  7269  f1ounsn  7276  isores3  7339  isoselem  7345  oprabv  7476  eloprabga  7525  sorpsscmpl  7737  difex2  7761  ordpwsuc  7813  ordsucun  7823  limuni3  7850  trom  7873  fo1stres  8014  poxp  8126  soxp  8127  xpord3inddlem  8152  soseq  8157  suppimacnv  8172  fsuppeq  8173  funsssuppss  8188  brtpos2  8230  frrlem8  8292  fpr2a  8301  onnseq  8333  smores  8341  smofvon2  8345  tfrlem1  8364  oacl  8522  omcl  8523  oecl  8524  oawordri  8537  oalimcl  8547  oaass  8548  oarec  8549  omwordri  8559  omeulem1  8569  omeulem2  8570  oeordi  8575  oeworde  8581  oeoelem  8586  nnacl  8599  nnmcl  8600  nnecl  8601  nnacom  8605  nnaass  8610  nnmsucr  8613  nnmordi  8619  omabs  8639  cofonr  8662  naddunif  8682  iiner  8789  elpmg  8842  fsetfcdm  8859  fsetprcnex  8861  pmss12g  8869  mapfvd  8879  f1domg  8970  ssdomg  8999  undom  9056  domtriord  9114  ssnnfi  9157  fnfi  9165  enfi  9174  php  9194  sdom1  9213  1sdom2dom  9217  fisseneq  9226  isinf  9228  dif1ennnALT  9240  findcard3  9246  frfi  9248  difinf  9274  iunfi  9303  fsuppunfi  9351  fsuppres  9356  ffsuppbi  9361  elfi2  9377  marypha1lem  9396  marypha1  9397  oiexg  9500  wemapso2  9518  harword  9528  brwdom  9532  unxpwdom  9554  en3lplem1  9584  inf3lemd  9599  inf3lem5  9604  cantnfval2  9641  cantnfle  9643  cantnflt  9644  cnfcom  9672  tcmin  9711  frr2  9735  r1sdom  9749  rankxplim3  9856  cardidm  9957  cardmin2  9997  infxpenlem  10009  fseqenlem1  10020  numacn  10045  alephordi  10070  iscard3  10089  alephinit  10091  carduniima  10092  iunfictbso  10110  dfac5  10124  dfac12lem3  10141  nnadju  10193  pwsdompw  10198  pwdjudom  10210  cflim2  10258  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  alephsing  10271  infpssALT  10308  fin23lem34  10341  isf32lem2  10349  isf32lem10  10357  isf32lem12  10359  isfin1-2  10380  hsmexlem4  10424  axcc2lem  10431  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  ac6num  10474  ac6s  10479  zorn2lem7  10497  ttukeylem5  10508  imadomg  10529  iundom2g  10535  ondomon  10558  ficard  10560  konigthlem  10564  alephreg  10578  pwcfsdom  10579  cfpwsdom  10580  axregndlem1  10598  axregnd  10600  pwfseqlem3  10656  pwxpndom2  10661  pwxpndom  10662  pwdjundom  10663  inawinalem  10685  gchina  10695  wuncval2  10743  tsk0  10759  tskxpss  10768  inatsk  10774  tskuni  10779  gruina  10814  grothac  10826  addclpi  10888  addnidpi  10897  nqereu  10925  mulcanenq  10956  genpnnp  11001  nqpr  11010  prlem934  11029  reclem2pr  11044  suplem1pr  11048  supsrlem  11107  axpre-sup  11165  1re  11219  dedekindle  11385  00id  11396  receu  11870  sup3  12183  infrelb  12211  peano5nni  12247  nnindd  12264  nnaddcl  12267  zrevaddcl  12650  nzadd  12653  zdiv  12677  nneo  12691  zeo2  12694  nn0indd  12704  fzind  12705  fnn0ind  12706  fzindd  12709  uzwo  12946  lbzbi  12971  nn01to3  12976  qrevaddcl  13006  irradd  13008  irrmul  13009  ltsubrp  13065  ltaddrp  13066  xnn0xaddcl  13272  xnn0xadd0  13284  icoshft  13511  fzen  13580  elfzm11  13635  uzsplit  13636  elfzom1elp1fzo  13773  fzoopth  13803  injresinjlem  13831  injresinj  13832  modifeq2int  13982  modsumfzodifsn  13993  om2uzlti  13999  ssnn0fi  14034  fsuppmapnn0fiub0  14042  mptnn0fsuppr  14048  seqcaopr3  14086  seqf1olem2a  14089  seqf1o  14092  ser1const  14107  expadd  14153  expmul  14156  leexp1a  14224  faccl  14332  facdiv  14336  faclbnd  14339  faclbnd4lem4  14345  hasheqf1oi  14400  hashgadd  14426  hashinfxadd  14434  hashunx  14435  hashunsng  14441  elprchashprn2  14445  hashss  14458  hash1snb  14469  hashmap  14485  hashf1lem2  14506  hashf1  14507  seqcoll  14514  hashle2pr  14527  hashdmpropge2  14533  hashge3el3dif  14537  hash1to3  14542  fundmge2nop0  14552  fi1uzind  14557  brfi1indALT  14560  sswrd  14572  swrdnd2  14710  swrdnnn0nd  14711  swrdnd0  14712  swrdwrdsymb  14717  pfxnd0  14743  swrdswrdlem  14758  swrdswrd  14759  wrd2ind  14777  swrdccatin1  14779  swrdccatin2  14783  pfxccatin12lem2  14785  pfxccat3  14788  repsdf2  14834  repswswrd  14840  cshw0  14850  cshwcl  14854  cshwlen  14855  cshf1  14866  swrdco  14893  relexpsucnnl  15086  rtrclreclem3  15116  rtrclreclem4  15117  relexpindlem  15119  rtrclind  15121  shftlem  15124  sgn3da  15157  caubnd  15429  reusq0  15535  rlimcld2  15648  o1dif  15700  climub  15732  climserle  15733  iseraltlem2  15753  sumss  15793  fsumzcl2  15808  fsummsnunz  15823  fsumsplitsnun  15824  fsum2d  15840  modfsummods  15863  fsumabs  15871  fsumrlim  15881  fsumo1  15882  fsumiun  15891  climcndslem1  15921  climcndslem2  15922  cvgrat  15955  clim2prod  15960  prodfn0  15966  prodfrec  15967  ntrivcvg  15969  prodmo  16008  fprodss  16020  fprodabs  16046  fprodn0  16051  fprod2d  16053  fprodefsum  16166  ruclem8  16310  ruclem9  16311  dvdsmod0  16333  dvds2ln  16364  dvdsaddre2b  16382  dvdslelem  16384  dvdsdivcl  16391  alzdvds  16395  mod2eq1n2dvds  16422  oddnn02np1  16423  nn0o1gt2  16456  nno  16457  sumeven  16462  sumodd  16463  pwp1fsum  16466  ndvdsadd  16485  bitsinv1  16517  sadcadd  16533  sadadd2  16535  saddisjlem  16539  smuval2  16557  smupvallem  16558  smu01lem  16560  smupval  16563  smueqlem  16565  smumullem  16567  gcddiv  16626  rplpwr  16633  nn0seqcvgd  16645  seq1st  16646  alginv  16650  algcvga  16654  algfx  16655  absprodnn  16693  isprm2  16757  isprm3  16758  prmind2  16760  maxprmfct  16785  prmdvdsexp  16791  pcmpt  16969  prmreclem4  16996  vdwmc2  17056  vdwlem10  17067  ramub2  17091  ramcl  17106  prmgaplem5  17132  prmgaplem8  17135  cshwshashlem1  17172  cshwshashlem3  17174  setsn0fun  17250  imasleval  17612  divsfval  17618  mreexexlem4d  17720  isssc  17894  initoeu1  18085  termoeu1  18092  istos  18489  chnfibg  18709  mgmcl  18718  sgrpidmnd  18818  frmdgsum  18944  smndex1mgm  18992  dfgrp3lem  19127  mhmmulg  19204  resghm2b  19327  gsumwrev  19459  elsymgbas  19467  symgextf1  19514  gsmsymgreqlem2  19524  gsmsymgreq  19525  odlem1  19628  odcl2  19658  gexlem1  19672  efgi2  19818  efginvrel2  19820  efgsrel  19827  cyggexb  19992  gsummulglem  20034  gsumzunsnd  20049  gsum2dlem2  20064  telgsums  20086  dmdprd  20093  dprdw  20105  ablfac1eulem  20167  srgpcomp  20323  rnghmmul  20556  nrhmzr  20665  lmodfopnelem1  21048  rmodislmodlem  21079  cnfldmulg  21583  cnfldexp  21584  nzerooringczr  21659  obslbs  21909  mplcoe1  22217  mplcoe3  22218  mplcoe5  22220  cply1mul  22485  coe1fzgsumdlem  22492  gsummoncoe1  22497  pf1ind  22544  evl1gsumdlem  22545  mat1dimcrng  22663  ma1repveval  22757  mulmarep1gsum2  22760  gsummatr01lem3  22843  cramerlem3  22875  decpmatmulsumfsupp  22959  mp2pm2mplem4  22995  pm2mpmhmlem1  23004  fvmptnn04if  23035  cayhamlem1  23052  fctop  23190  mretopd  23278  restopnb  23361  restdis  23364  tgcnp  23439  cncls2  23459  cncls  23460  cnntr  23461  cnsscnp  23465  cmpsub  23586  2ndcsep  23645  1stcelcls  23647  lfinpfin  23710  locfincmp  23712  comppfsc  23718  txcn  23812  txlm  23834  xkohaus  23839  qtopres  23884  haushmphlem  23973  cmphmph  23974  connhmph  23975  reghmph  23979  nrmhmph  23980  ptcmpfi  23999  reghaus  24011  fbssfi  24023  fbun  24026  fbfinnfr  24027  isfildlem  24043  fgcl  24064  cfinfil  24079  supfil  24081  ufinffr  24115  fin1aufil  24118  cnpflf  24187  alexsubALTlem3  24235  alexsubALT  24237  cnextfvval  24251  cnextcn  24253  tmdgsum  24281  tgphaus  24303  tgpt1  24304  mettri  24538  blssexps  24612  blssex  24613  mopni3  24680  metss  24694  psmetutop  24753  dscmet  24758  tngngp3  24842  rectbntr0  25019  metnrmlem1a  25045  fsumcn  25058  lmmbr  25446  caubl  25496  caublcls  25497  bcthlem5  25516  bcth3  25519  ovolunlem1a  25684  ovoliunnul  25695  finiunmbl  25732  voliunlem1  25738  volsuplem  25743  volsup  25744  dyadmax  25786  itgfsum  26015  dvnadd  26117  cpnord  26123  dvnfre  26140  dvmptfsum  26163  dvlip  26181  fta1g  26356  plyco  26427  dgrcolem1  26459  dgrco  26461  dvnply2  26477  plydivex  26487  plyexmo  26503  aannenlem1  26520  aaliou3lem2  26535  dvntaylp  26563  taylthlem1  26565  ulmval  26572  cxpmul2  26883  cxpsqrtth  26924  scvxcvx  27179  jensenlem2  27181  jensen  27182  ppiub  27397  bcmono  27470  bpos1lem  27475  bposlem5  27481  gausslemma2dlem6  27565  lgsquad2lem2  27578  2lgslem3  27597  2lgs  27600  2sqnn  27632  addsqnreup  27636  2sqreultblem  27641  2sqreunnltblem  27644  dchrisumlem1  27682  dchrisum0flb  27703  pntpbnd1  27779  pntlemf  27798  qabvle  27818  qabvexp  27819  ostthlem2  27821  ostth2lem2  27827  ltsval2  27849  ltssolem1  27868  negsprop  28257  mulsuniflem  28371  precsexlem6  28434  precsexlem7  28435  noseqind  28514  om2noseqlt  28521  n0addscl  28566  n0mulscl  28567  expsne0  28658  axeuclidlem  29341  axcontlem12  29354  umgrnloopv  29485  uhgredgrnv  29509  edglnl  29522  numedglnl  29523  usgruspgrb  29562  usgrnloopvALT  29580  usgredg2vlem2  29605  subupgr  29666  nbumgr  29726  uhgrnbgr0nb  29733  nbgr0edglem  29735  edgusgrnbfin  29752  nb3grprlem2  29760  uvtxnbgrvtx  29772  cplgrop  29816  cusgrfi  29837  fusgrmaxsize  29843  fusgrn0degnn0  29878  ewlkprop  29982  uspgr2wlkeq  30024  g0wlk0  30029  wlkreslem  30046  lfgriswlk  30065  upgrwlkdvde  30115  spthonepeq  30130  uhgrwkspth  30133  usgr2trlncl  30138  usgr2trlspth  30139  cyclnumvtx  30178  cyclnspth  30179  crctcshwlkn0lem3  30190  wwlksn  30215  wspthneq1eq2  30238  wwlksm1edg  30259  wwlksnred  30270  wwlksnextfun  30276  wwlksnextinj  30277  wwlksnextproplem3  30289  wspthsnonn0vne  30295  wspn0  30302  rusgrnumwwlk  30356  clwwlkccatlem  30369  umgrclwwlkge2  30371  clwlkclwwlklem2  30380  clwlkclwwlklem3  30381  clwwisshclwws  30395  clwwisshclwwsn  30396  clwwlkn1loopb  30423  wwlksext2clwwlk  30437  wwlksubclwwlk  30438  clwwlknonex2lem2  30488  upgr3v3e3cycl  30560  uhgr3cyclex  30562  upgr4cycl4dv4e  30565  eupth2lem3lem4  30611  eupth2lem3lem7  30614  eupth2  30619  eulerpath  30621  nfrgr2v  30652  frgr3vlem1  30653  3vfriswmgr  30658  1to2vfriswmgr  30659  1to3vfriswmgr  30660  3cyclfrgrrn1  30665  3cyclfrgrrn  30666  3cyclfrgrrn2  30667  4cycl2vnunb  30670  frgrncvvdeqlem2  30680  frgrncvvdeqlem8  30686  frgrncvvdeqlem9  30687  frgrwopreglem4a  30690  frgrwopreglem5lem  30700  frgrwopreglem5ALT  30702  frgrregorufr0  30704  frgr2wwlk1  30709  frgr2wwlkeqm  30711  fusgr2wsp2nb  30714  2wspmdisj  30717  frrusgrord  30721  numclwwlk1lem2f1  30737  numclwlk1  30751  frgrreggt1  30773  friendshipgt3  30778  hlim2  31573  elnlfn  32309  stle0i  32620  hstrbi  32647  spansncv2  32674  h1da  32730  fmptcof2  33031  xreceu  33270  domnprodn0  33621  1arithufdlem3  33859  1arithufdlem4  33860  tpr2rico  34325  hasheuni  34498  ismeas  34613  sseqp1  34809  rrvsum  34868  dstfrvunirn  34889  signstfvc  34985  bnj607  35328  bnj1145  35405  bnj1204  35424  r1filim  35515  fineqvrep  35543  fineqvnttrclselem1  35550  onvf1odlem4  35606  vonf1oonfo  35615  fisshasheq  35621  subgrwlk  35637  subfacp1lem6  35690  cvmlift2lem12  35819  cvmlift3lem4  35827  satfrnmapom  35875  sat1el2xp  35884  satffunlem2  35913  satffun  35914  mrsubvrs  36027  climuzcnv  36176  iprodefisumlem  36245  dfon2lem9  36294  linethru  36658  elhf2  36680  finminlem  36862  fnessref  36901  neibastop2lem  36904  fnemeet2  36911  nndivsub  37001  mh-inf3f1  37085  bj-cbvew  37297  bj-xpnzex  37628  bj-elpwg  37721  bj-epelg  37737  bj-axseprep  37744  mptsnunlem  38017  dissneqlem  38019  topdifinffinlem  38026  iooelexlt  38041  domalom  38083  fvineqsneq  38091  wl-exeq  38222  matunitlindflem1  38300  poimirlem22  38326  poimirlem26  38330  poimirlem28  38332  poimirlem29  38333  poimirlem32  38336  heicant  38339  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  cover2  38399  upixp  38413  sdclem2  38426  fdc  38429  seqpo  38431  metf1o  38439  mettrifi  38441  sstotbnd3  38460  heibor1lem  38493  heiborlem5  38499  heibor  38505  bfplem1  38506  elghomlem2OLD  38570  grpokerinj  38577  isrngo  38581  rngodm1dm2  38616  ispridl2  38722  exlimddvf  38803  lssatle  39822  4atexlemex4  40880  uzindd  42778  evl1gprodd  42917  sn-axprlem3  43022  redvmptabs  43154  sn-sup3d  43299  mzpsubst  43512  jm2.18  43748  wepwsolem  43802  oaabsb  44054  oacl2g  44090  ofoafg  44114  ofoaid1  44118  ofoaid2  44119  naddonnn  44155  iunrelexp0  44461  relexpmulg  44469  cnvtrclfv  44483  clsk1indlem3  44802  grucollcld  45003  inaex  45040  dvgrat  45055  radcnvrat  45057  csbxpgVD  45635  sineq0ALT  45678  trfr  45704  relwf  45709  pwclaxpow  45726  omssaxinf2  45730  islptre  46368  iblspltprt  46720  stoweidlem2  46749  stoweidlem17  46764  stoweidlem21  46768  2reuimp0  47884  2reuimp  47885  afveu  47923  funbrafv  47928  ndmaovass  47976  afv2eu  48008  tz6.12c-afv2  48012  funop1  48053  f1oresf1o2  48061  fvmptrabdm  48063  nltle2tri  48083  2elfz2melfz  48088  fsummsndifre  48150  fsumsplitsndif  48151  fsummmodsndifre  48152  fsummmodsnunz  48153  elsetpreimafvssdm  48168  uniimaelsetpreimafv  48178  imasetpreimafvbijlemfv1  48185  iccpartiltu  48204  iccpartigtl  48205  iccpartleu  48210  iccpartgel  48211  iccpartrn  48212  iccpartiun  48216  icceuelpart  48218  iccpartnel  48220  fargshiftf  48222  fargshiftf1  48223  ichnfb  48247  elsprel  48257  prsprel  48269  sprsymrelfo  48279  paireqne  48293  sbcpr  48303  reupr  48304  fmtnoinf  48321  odz2prm2pw  48348  lighneallem4  48395  lighneal  48396  requad1  48420  requad2  48421  evensumeven  48505  even3prm2  48517  gbowgt5  48560  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbnnsum3prm  48602  bgoldbtbndlem2  48604  bgoldbtbndlem4  48606  bgoldbtbnd  48607  dfsclnbgr6  48656  grimco  48687  cycl3grtri  48745  isubgr3stgrlem6  48769  gricgrlic  48816  gpgedgvtx0  48859  gpgprismgr4cycllem3  48895  pgnbgreunbgrlem5  48921  clcllaw  48989  rngccatidALTV  49070  ringccatidALTV  49104  scmsuppss  49184  gsumlsscl  49193  ply1mulgsumlem2  49200  lincvalsc0  49234  linc0scn0  49236  lincdifsn  49237  linc1  49238  lincellss  49239  lincsum  49242  lincscm  49243  lincsumcl  49244  lcoss  49249  lincext3  49269  lindslinindimp2lem4  49274  lindslinindsimp2lem5  49275  lindslinindsimp2  49276  lindsrng01  49281  snlindsntor  49284  lincresunit3lem2  49293  lincresunit3  49294  islindeps2  49296  blengt1fldiv2p1  49406  2arymaptf1  49466  resum2sqorgt0  49522  reorelicc  49523  rrx2plordisom  49536  rrx2linest  49555  rrxsphere  49561  line2ylem  49564  itsclc0xyqsol  49581  itscnhlinecirc02p  49598  mo0sn  49627  thincn0eu  50242  alsralrex  50623  alsraln0  50624