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  2134  mo4  2594  2moswapv  2657  2moswap  2672  2eu2  2680  pm2.61ne  3044  nelelne  3060  r19.21be  3259  rspcebdv  3574  2reu2  3850  csbie2df  4404  minel  4422  uneqdifeq  4451  raltpd  4744  ssunsn2  4788  opthprneg  4825  ssuni  4898  uniss2  4907  elpwuni  5070  intss2  5073  disjord  5097  elpw2g  5302  elssabg  5311  axprglem  5401  oteqex  5479  otsndisj  5499  otiunsndisj  5500  epelg  5559  wereu  5654  relop  5838  riinint  5966  sotri3  6142  unixpid  6311  reuop  6322  ordtr2  6434  ordsssuc2  6482  iotan0  6555  iotan0OLD  6556  funopg  6602  fun  6774  fvmptnf  7047  fvn0ssdmfun  7106  eldmrexrnb  7124  fmptco  7162  fnressn  7194  fressnfv  7196  fprb  7230  fvtp2g  7235  fvtp3g  7236  fconst2g  7240  fntpb  7246  f1dom3el3dif  7304  f1ounsn  7311  isores3  7374  isoselem  7380  oprabv  7511  eloprabga  7560  sorpsscmpl  7782  difex2  7806  ordpwsuc  7860  ordsucun  7870  limuni3  7897  trom  7920  fo1stres  8061  poxp  8177  soxp  8178  xpord3inddlem  8208  soseq  8213  suppimacnv  8229  fsuppeq  8230  funsssuppss  8245  brtpos2  8287  frrlem8  8349  fpr2a  8358  onnseq  8390  smores  8398  smofvon2  8402  tfrlem1  8421  oacl  8581  omcl  8582  oecl  8583  oawordri  8596  oalimcl  8606  oaass  8607  oarec  8608  omwordri  8618  omeulem1  8628  omeulem2  8629  oeordi  8634  oeworde  8640  oeoelem  8645  nnacl  8658  nnmcl  8659  nnecl  8660  nnacom  8664  nnaass  8669  nnmsucr  8672  nnmordi  8678  omabs  8698  cofonr  8721  naddunif  8741  iiner  8848  elpmg  8901  fsetfcdm  8920  fsetprcnex  8922  pmss12g  8935  mapfvd  8945  f1domg  9036  ssdomg  9065  undom  9122  domtriord  9180  ssnnfi  9223  fnfi  9231  enfi  9240  php  9260  sdom1  9279  1sdom2dom  9283  fisseneq  9292  isinf  9294  dif1ennnALT  9306  findcard3  9312  frfi  9314  difinf  9341  iunfi  9370  fsuppunfi  9417  fsuppres  9422  ffsuppbi  9427  elfi2  9443  marypha1lem  9462  marypha1  9463  oiexg  9566  wemapso2  9584  harword  9594  brwdom  9598  unxpwdom  9620  en3lplem1  9650  inf3lemd  9665  inf3lem5  9670  cantnfval2  9707  cantnfle  9709  cantnflt  9710  cnfcom  9738  tcmin  9777  frr2  9801  r1sdom  9818  rankxplim3  9935  elhf2  9947  elhf3OLD  9960  hfpw  9963  cardidm  10077  cardmin2  10119  infxpenlem  10131  fseqenlem1  10142  numacn  10167  alephordi  10192  iscard3  10211  alephinit  10213  carduniima  10214  iunfictbso  10232  dfac5  10246  dfac12lem3  10263  nnadju  10315  pwsdompw  10320  pwdjudom  10332  cflim2  10380  cfslb2n  10385  cofsmo  10386  cfsmolem  10387  cfcoflem  10389  alephsing  10393  infpssALT  10430  fin23lem34  10463  isf32lem2  10471  isf32lem10  10479  isf32lem12  10481  isfin1-2  10502  hsmexlem4  10546  axcc2lem  10553  domtriomlem  10559  axdc2lem  10565  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  axcclem  10574  ac6num  10596  ac6s  10601  zorn2lem7  10619  ttukeylem5  10630  imadomg  10652  iundom2g  10663  ondomon  10686  ficard  10688  konigthlem  10692  alephreg  10706  pwcfsdom  10707  cfpwsdom  10708  axregndlem1  10726  axregnd  10728  pwfseqlem3  10784  pwxpndom2  10789  pwxpndom  10790  pwdjundom  10791  inawinalem  10813  gchina  10823  wuncval2  10871  tsk0  10887  tskxpss  10896  inatsk  10902  tskuni  10907  gruina  10942  grothac  10954  addclpi  11016  addnidpi  11025  nqereu  11053  mulcanenq  11084  genpnnp  11129  nqpr  11138  prlem934  11157  reclem2pr  11172  suplem1pr  11176  supsrlem  11235  axpre-sup  11293  1re  11347  dedekindle  11513  00id  11524  receu  12001  sup3  12314  infrelb  12342  peano5nni  12378  nnindd  12395  nnaddcl  12398  zrevaddcl  12781  nzadd  12784  zdiv  12809  nneo  12823  zeo2  12826  nn0indd  12836  fzind  12837  fnn0ind  12838  fzindd  12841  uzwo  13078  lbzbi  13103  nn01to3  13108  qrevaddcl  13139  irradd  13141  irrmul  13142  ltsubrp  13198  ltaddrp  13199  xnn0xaddcl  13405  xnn0xadd0  13417  icoshft  13644  fzen  13714  elfzm11  13769  uzsplit  13770  elfzom1elp1fzo  13907  fzoopth  13937  injresinjlem  13965  injresinj  13966  modifeq2int  14116  modsumfzodifsn  14127  om2uzlti  14133  ssnn0fi  14168  fsuppmapnn0fiub0  14176  mptnn0fsuppr  14182  seqcaopr3  14220  seqf1olem2a  14223  seqf1o  14226  ser1const  14241  expadd  14287  expmul  14290  leexp1a  14358  faccl  14468  facdiv  14472  faclbnd  14475  faclbnd4lem4  14481  hasheqf1oi  14536  hashgadd  14562  hashinfxadd  14570  hashunx  14571  hashunsng  14577  elprchashprn2  14581  hashss  14594  hash1snb  14605  hashmap  14621  hashf1lem2  14642  hashf1  14643  seqcoll  14650  hashle2pr  14663  hashdmpropge2  14669  hashge3el3dif  14673  hash1to3  14678  fundmge2nop0  14688  fi1uzind  14693  brfi1indALT  14696  sswrd  14708  swrdnd2  14847  swrdnnn0nd  14848  swrdnd0  14849  swrdwrdsymb  14854  pfxnd0  14880  swrdswrdlem  14895  swrdswrd  14896  wrd2ind  14914  swrdccatin1  14916  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccat3  14925  repsdf2  14971  repswswrd  14977  cshw0  14987  cshwcl  14991  cshwlen  14992  cshf1  15003  swrdco  15030  relexpsucnnl  15226  rtrclreclem3  15256  rtrclreclem4  15257  relexpindlem  15259  rtrclind  15261  shftlem  15264  sgn3da  15297  caubnd  15570  reusq0  15676  rlimcld2  15789  o1dif  15841  climub  15873  climserle  15874  iseraltlem2  15894  sumss  15934  fsumzcl2  15949  fsummsnunz  15964  fsumsplitsnun  15965  fsum2d  15981  modfsummods  16004  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  climcndslem1  16062  climcndslem2  16063  cvgrat  16096  clim2prod  16101  prodfn0  16107  prodfrec  16108  ntrivcvg  16110  prodmo  16147  fprodss  16159  fprodabs  16185  fprodn0  16190  fprod2d  16192  fprodefsum  16305  ruclem8  16449  ruclem9  16450  dvdsmod0  16472  dvds2ln  16503  dvdsaddre2b  16521  dvdslelem  16523  dvdsdivcl  16530  alzdvds  16534  mod2eq1n2dvds  16561  oddnn02np1  16562  nn0o1gt2  16595  nno  16596  sumeven  16601  sumodd  16602  pwp1fsum  16605  ndvdsadd  16624  bitsinv1  16656  sadcadd  16672  sadadd2  16674  saddisjlem  16678  smuval2  16696  smupvallem  16697  smu01lem  16699  smupval  16702  smueqlem  16704  smumullem  16706  gcddiv  16768  rplpwr  16776  nn0seqcvgd  16789  seq1st  16790  alginv  16794  algcvga  16798  algfx  16799  absprodnn  16837  isprm2  16901  isprm3  16902  prmind2  16904  maxprmfct  16929  prmdvdsexp  16935  pcmpt  17114  prmreclem4  17141  vdwmc2  17201  vdwlem10  17212  ramub2  17236  ramcl  17251  prmgaplem5  17277  prmgaplem8  17280  cshwshashlem1  17317  cshwshashlem3  17319  setsn0fun  17395  imasleval  17763  divsfval  17769  mreexexlem4d  17871  isssc  18045  initoeu1  18236  termoeu1  18243  istos  18640  chnfibg  18860  mgmcl  18869  frmdgsum  19108  smndex1mgm  19156  dfgrp3lem  19298  mhmmulg  19375  resghm2b  19498  gsumwrev  19631  elsymgbas  19639  symgextf1  19686  gsmsymgreqlem2  19696  gsmsymgreq  19697  odlem1  19800  odcl2  19830  gexlem1  19844  efgi2  19990  efginvrel2  19992  efgsrel  19999  cyggexb  20164  gsummulglem  20206  gsumzunsnd  20221  gsum2dlem2  20236  telgsums  20258  dmdprd  20265  dprdw  20277  ablfac1eulem  20339  srgpcomp  20495  rnghmmul  20730  nrhmzr  20840  lmodfopnelem1  21224  rmodislmodlem  21255  cnfldmulg  21762  cnfldexp  21763  nzerooringczr  21841  obslbs  22091  mplcoe1  22401  mplcoe3  22402  mplcoe5  22404  cply1mul  22669  coe1fzgsumdlem  22676  gsummoncoe1  22681  pf1ind  22728  evl1gsumdlem  22729  mat1dimcrng  22847  ma1repveval  22941  mulmarep1gsum2  22944  gsummatr01lem3  23027  matunitlindflem1  23049  cramerlem3  23062  decpmatmulsumfsupp  23146  mp2pm2mplem4  23182  pm2mpmhmlem1  23191  fvmptnn04if  23222  cayhamlem1  23239  fctop  23377  mretopd  23465  restopnb  23548  restdis  23551  tgcnp  23626  cncls2  23646  cncls  23647  cnntr  23648  cnsscnp  23652  cmpsub  23773  2ndcsep  23833  1stcelcls  23835  lfinpfin  23898  locfincmp  23900  comppfsc  23906  txcn  24000  txlm  24022  xkohaus  24027  qtopres  24072  haushmphlem  24161  cmphmph  24162  connhmph  24163  reghmph  24167  nrmhmph  24168  ptcmpfi  24187  reghaus  24199  fbssfi  24211  fbun  24214  fbfinnfr  24215  isfildlem  24231  fgcl  24252  cfinfil  24267  supfil  24269  ufinffr  24303  fin1aufil  24306  cnpflf  24375  alexsubALTlem3  24423  alexsubALT  24425  cnextfvval  24439  cnextcn  24441  tmdgsum  24469  tgphaus  24491  tgpt1  24492  mettri  24726  blssexps  24800  blssex  24801  mopni3  24868  metss  24882  psmetutop  24941  dscmet  24946  tngngp3  25030  rectbntr0  25207  metnrmlem1a  25233  fsumcn  25246  lmmbr  25634  caubl  25684  caublcls  25685  bcthlem5  25704  bcth3  25707  ovolunlem1a  25872  ovoliunnul  25883  finiunmbl  25920  voliunlem1  25926  volsuplem  25931  volsup  25932  dyadmax  25974  itgfsum  26202  dvnadd  26304  cpnord  26310  dvnfre  26327  dvmptfsum  26350  dvlip  26368  fta1g  26543  plyco  26615  dgrcolem1  26647  dgrco  26649  dvnply2  26663  plydivex  26673  plyexmo  26691  aannenlem1  26712  aaliou3lem2  26727  dvntaylp  26755  taylthlem1  26757  ulmval  26764  cxpmul2  27074  cxpsqrtth  27115  scvxcvx  27370  jensenlem2  27372  jensen  27373  ppiub  27588  bcmono  27661  bpos1lem  27666  bposlem5  27672  gausslemma2dlem6  27756  lgsquad2lem2  27769  2lgslem3  27788  2lgs  27791  2sqnn  27823  addsqnreup  27827  2sqreultblem  27832  2sqreunnltblem  27835  dchrisumlem1  27873  dchrisum0flb  27894  pntpbnd1  27970  pntlemf  27989  qabvle  28009  qabvexp  28010  ostthlem2  28012  ostth2lem2  28018  ltsval2  28070  ltssolem1  28089  negsprop  28478  mulsuniflem  28592  precsexlem6  28655  precsexlem7  28656  noseqind  28735  om2noseqlt  28742  n0addscl  28787  n0mulscl  28788  expsne0  28879  axeuclidlem  29597  axcontlem12  29610  umgrnloopv  29741  uhgredgrnv  29765  edglnl  29778  numedglnl  29779  usgruspgrb  29821  usgrnloopvALT  29839  usgredg2vlem2  29864  subupgr  29925  nbumgr  29985  uhgrnbgr0nb  29992  nbgr0edglem  29994  edgusgrnbfin  30011  nb3grprlem2  30019  uvtxnbgrvtx  30031  cplgrop  30075  cusgrfi  30096  fusgrmaxsize  30102  fusgrn0degnn0  30137  ewlkprop  30241  uspgr2wlkeq  30283  g0wlk0  30288  wlkreslem  30305  subgrwlk  30326  lfgriswlk  30328  upgrwlkdvde  30380  spthonepeq  30395  uhgrwkspth  30398  usgr2trlncl  30403  usgr2trlspth  30404  cyclnumvtx  30445  cyclnspth  30446  crctcshwlkn0lem3  30458  wwlksn  30483  wspthneq1eq2  30506  wwlksm1edg  30527  wwlksnred  30538  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextproplem3  30557  wspthsnonn0vne  30563  wspn0  30570  rusgrnumwwlk  30624  clwwlkccatlem  30637  umgrclwwlkge2  30639  clwlkclwwlklem2  30648  clwlkclwwlklem3  30649  clwwisshclwws  30663  clwwisshclwwsn  30664  clwwlkn1loopb  30691  wwlksext2clwwlk  30705  wwlksubclwwlk  30706  clwwlknonex2lem2  30756  upgr3v3e3cycl  30838  uhgr3cyclex  30840  upgr4cycl4dv4e  30843  eupth2lem3lem4  30889  eupth2lem3lem7  30892  eupth2  30897  eulerpath  30899  nfrgr2v  30930  frgr3vlem1  30931  3vfriswmgr  30936  1to2vfriswmgr  30937  1to3vfriswmgr  30938  3cyclfrgrrn1  30943  3cyclfrgrrn  30944  3cyclfrgrrn2  30945  4cycl2vnunb  30948  frgrncvvdeqlem2  30958  frgrncvvdeqlem8  30964  frgrncvvdeqlem9  30965  frgrwopreglem4a  30968  frgrwopreglem5lem  30978  frgrwopreglem5ALT  30980  frgrregorufr0  30982  frgr2wwlk1  30987  frgr2wwlkeqm  30989  fusgr2wsp2nb  30992  2wspmdisj  30995  frrusgrord  30999  numclwwlk1lem2f1  31015  numclwlk1  31029  frgrreggt1  31051  friendshipgt3  31056  hlim2  31851  elnlfn  32587  stle0i  32898  hstrbi  32925  spansncv2  32952  h1da  33008  fmptcof2  33349  xreceu  33584  domnprodn0  33938  1arithufdlem3  34182  1arithufdlem4  34183  tpr2rico  34655  hasheuni  34828  ismeas  34943  sseqp1  35138  rrvsum  35197  dstfrvunirn  35218  signstfvc  35314  bnj607  35657  bnj1145  35734  bnj1204  35753  dfac15  35886  dfac16  35887  acwer1prclem  35892  fineqvrep  35923  fineqvnttrclselem1  35930  j0ltaleph  36049  onvf1odlem4  36075  onprcf1acwevdlem1  36086  vonf1oonfo  36090  fisshasheq  36101  srepdflem2  36127  subfacp1lem6  36158  cvmlift2lem12  36287  cvmlift3lem4  36295  satfrnmapom  36343  sat1el2xp  36352  satffunlem2  36381  satffun  36382  mrsubvrs  36495  climuzcnv  36644  iprodefisumlem  36720  dfon2lem9  36768  linethru  37133  finminlem  37321  fnessref  37360  neibastop2lem  37363  fnemeet2  37370  nndivsub  37460  bj-cbvew  37756  bj-xpnzex  38087  bj-elpwg  38237  bj-epelg  38253  bj-axseprep  38260  mptsnunlem  38529  dissneqlem  38531  topdifinffinlem  38538  iooelexlt  38553  domalom  38595  fvineqsneq  38603  wl-exeq  38734  poimirlem22  38828  poimirlem26  38832  poimirlem28  38834  poimirlem29  38835  poimirlem32  38838  heicant  38841  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  cover2  38917  upixp  38931  sdclem2  38942  fdc  38945  seqpo  38947  metf1o  38955  mettrifi  38957  sstotbnd3  38976  heibor1lem  39009  heiborlem5  39015  heibor  39021  bfplem1  39022  elghomlem2OLD  39086  grpokerinj  39093  isrngo  39097  rngodm1dm2  39132  ispridl2  39238  exlimddvf  39319  lssatle  40338  4atexlemex4  41396  uzindd  43294  evl1gprodd  43433  sn-axprlem3  43539  redvmptabs  43677  sn-sup3d  43822  mzpsubst  44025  jm2.18  44261  wepwsolem  44315  oaabsb  44557  oacl2g  44593  ofoafg  44617  ofoaid1  44621  ofoaid2  44622  naddonnn  44658  iunrelexp0  44963  relexpmulg  44971  cnvtrclfv  44985  clsk1indlem3  45304  grucollcld  45505  inaex  45542  dvgrat  45557  radcnvrat  45559  csbxpgVD  46136  sineq0ALT  46179  trfr  46216  relwf  46221  pwclaxpow  46238  omssaxinf2  46242  islptre  46904  iblspltprt  47256  stoweidlem2  47285  stoweidlem17  47300  stoweidlem21  47304  aiotaexim  48441  2reuimp0  48458  2reuimp  48459  afveu  48496  funbrafv  48501  ndmaovass  48549  afv2eu  48581  tz6.12c-afv2  48585  funop1  48626  f1oresf1o2  48634  fvmptrabdm  48636  nltle2tri  48656  2elfz2melfz  48661  fsummsndifre  48723  fsumsplitsndif  48724  fsummmodsndifre  48725  fsummmodsnunz  48726  elsetpreimafvssdm  48741  uniimaelsetpreimafv  48751  imasetpreimafvbijlemfv1  48758  iccpartiltu  48777  iccpartigtl  48778  iccpartleu  48783  iccpartgel  48784  iccpartrn  48785  iccpartiun  48789  icceuelpart  48791  iccpartnel  48793  fargshiftf  48795  fargshiftf1  48796  ichnfb  48820  elsprel  48830  prsprel  48842  sprsymrelfo  48852  paireqne  48866  sbcpr  48876  reupr  48877  fmtnoinf  48894  odz2prm2pw  48921  lighneallem4  48968  lighneal  48969  requad1  48993  requad2  48994  evensumeven  49078  even3prm2  49090  gbowgt5  49133  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbnnsum3prm  49175  bgoldbtbndlem2  49177  bgoldbtbndlem4  49179  bgoldbtbnd  49180  dfsclnbgr6  49229  grimco  49260  cycl3grtri  49318  isubgr3stgrlem6  49342  gricgrlic  49389  gpgedgvtx0  49432  gpgprismgr4cycllem3  49468  pgnbgreunbgrlem5  49494  clcllaw  49561  rngccatidALTV  49642  ringccatidALTV  49676  scmsuppss  49814  gsumlsscl  49823  ply1mulgsumlem2  49830  lincvalsc0  49864  linc0scn0  49866  lincdifsn  49867  linc1  49868  lincellss  49869  lincsum  49872  lincscm  49873  lincsumcl  49874  lcoss  49879  lincext3  49899  lindslinindimp2lem4  49904  lindslinindsimp2lem5  49905  lindslinindsimp2  49906  lindsrng01  49911  snlindsntor  49914  lincresunit3lem2  49923  lincresunit3  49924  islindeps2  49926  blengt1fldiv2p1  50036  2arymaptf1  50096  resum2sqorgt0  50152  reorelicc  50153  rrx2plordisom  50167  rrx2linest  50185  rrxsphere  50191  line2ylem  50194  itsclc0xyqsol  50211  itscnhlinecirc02p  50228  mo0sn  50258  thincn0eu  50897  alsralrex  51336  alsraln0  51337