Theorem expcom 413

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancoms  458  pm3.21  471  sylan  580  animpimp2impd  846  4casesdan  1041  dedlema  1045  dedlemb  1046  sbiedvw  2095  mo4  2565  2moswapv  2628  2moswap  2643  2mosOLD  2649  2eu2  2652  pm2.61ne  3017  nelelne  3031  r19.21be  3235  cbvraldva2  3327  rspcebdv  3595  2reu2  3873  csbie2df  4418  minel  4441  uneqdifeq  4468  raltpd  4757  ssunsn2  4803  opthprneg  4841  ssuni  4908  uniss2  4917  elpwuni  5081  intss2  5084  disjord  5108  elpw2g  5303  elssabg  5313  axprlem3OLD  5398  axprlem4OLD  5399  axprlem5OLD  5400  oteqex  5475  otsndisj  5494  otiunsndisj  5495  epelg  5554  wereu  5650  relop  5830  riinint  5951  sotri3  6119  unixpid  6273  reuop  6282  ordtr2  6397  ordsssuc2  6444  iotan0  6520  funopg  6569  fun  6739  tz6.12cOLD  6902  fvmptnf  7007  fvn0ssdmfun  7063  eldmrexrnb  7081  fmptco  7118  fnressn  7147  fressnfv  7149  fprb  7185  fvtp2g  7190  fvtp3g  7191  fconst2g  7194  fntpb  7200  f1dom3el3dif  7261  f1ounsn  7264  isores3  7327  isoselem  7333  oprabv  7465  eloprabga  7514  sorpsscmpl  7726  difex2  7752  ordpwsuc  7807  ordsucun  7817  limuni3  7845  trom  7868  fo1stres  8012  poxp  8125  soxp  8126  xpord3inddlem  8151  soseq  8156  suppimacnv  8171  fsuppeq  8172  funsssuppss  8187  brtpos2  8229  frrlem8  8290  fpr2a  8299  wfrlem12OLD  8332  onnseq  8356  smores  8364  smofvon2  8368  tfrlem1  8388  oacl  8545  omcl  8546  oecl  8547  oawordri  8560  oalimcl  8570  oaass  8571  oarec  8572  omwordri  8582  omeulem1  8592  omeulem2  8593  oeordi  8597  oeworde  8603  oeoelem  8608  nnacl  8621  nnmcl  8622  nnecl  8623  nnacom  8627  nnaass  8632  nnmsucr  8635  nnmordi  8641  omabs  8661  cofonr  8684  naddunif  8703  iiner  8801  elpmg  8855  fsetfcdm  8872  fsetprcnex  8874  pmss12g  8881  mapfvd  8891  f1domg  8984  ssdomg  9012  undom  9071  domtriord  9135  ssnnfi  9181  fnfi  9190  enfi  9199  php  9219  phpOLD  9229  php3OLD  9231  sdom1  9248  1sdom2dom  9253  1sdomOLD  9255  fisseneq  9263  isinf  9266  isinfOLD  9267  dif1ennnALT  9281  findcard3  9288  findcard3OLD  9289  frfi  9291  difinf  9319  imafiOLD  9324  iunfi  9353  fsuppunfi  9398  fsuppres  9403  ffsuppbi  9408  elfi2  9424  marypha1lem  9443  marypha1  9444  oiexg  9547  wemapso2  9565  harword  9575  brwdom  9579  unxpwdom  9601  en3lplem1  9624  inf3lemd  9639  inf3lem5  9644  cantnfval2  9681  cantnfle  9683  cantnflt  9684  cnfcom  9712  tcmin  9753  frr2  9772  r1sdom  9786  rankxplim3  9893  cardidm  9971  cardmin2  10011  infxpenlem  10025  fseqenlem1  10036  numacn  10061  alephordi  10086  iscard3  10105  alephinit  10107  carduniima  10108  iunfictbso  10126  dfac5  10141  dfac12lem3  10158  nnadju  10210  pwsdompw  10215  pwdjudom  10227  cflim2  10275  cfslb2n  10280  cofsmo  10281  cfsmolem  10282  cfcoflem  10284  alephsing  10288  infpssALT  10325  fin23lem34  10358  isf32lem2  10366  isf32lem10  10374  isf32lem12  10376  isfin1-2  10397  hsmexlem4  10441  axcc2lem  10448  domtriomlem  10454  axdc2lem  10460  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  axcclem  10469  ac6num  10491  ac6s  10496  zorn2lem7  10514  ttukeylem5  10525  imadomg  10546  iundom2g  10552  ondomon  10575  ficard  10577  konigthlem  10580  alephreg  10594  pwcfsdom  10595  cfpwsdom  10596  axregndlem1  10614  axregnd  10616  pwfseqlem3  10672  pwxpndom2  10677  pwxpndom  10678  pwdjundom  10679  inawinalem  10701  gchina  10711  wuncval2  10759  tsk0  10775  tskxpss  10784  inatsk  10790  tskuni  10795  gruina  10830  grothac  10842  addclpi  10904  addnidpi  10913  nqereu  10941  mulcanenq  10972  genpnnp  11017  nqpr  11026  prlem934  11045  reclem2pr  11060  suplem1pr  11064  supsrlem  11123  axpre-sup  11181  1re  11233  dedekindle  11397  00id  11408  receu  11880  sup3  12197  infrelb  12225  peano5nni  12241  nnindd  12258  nnaddcl  12261  zrevaddcl  12635  nzadd  12638  zdiv  12661  nneo  12675  zeo2  12678  nn0indd  12688  fzind  12689  fnn0ind  12690  fzindd  12693  uzwo  12925  lbzbi  12950  nn01to3  12955  qrevaddcl  12985  irradd  12987  irrmul  12988  ltsubrp  13043  ltaddrp  13044  xnn0xaddcl  13249  xnn0xadd0  13261  icoshft  13488  fzen  13556  elfzm11  13610  uzsplit  13611  elfzom1elp1fzo  13746  fzoopth  13776  injresinjlem  13801  injresinj  13802  modifeq2int  13949  modsumfzodifsn  13960  om2uzlti  13966  ssnn0fi  14001  fsuppmapnn0fiub0  14009  mptnn0fsuppr  14015  seqcaopr3  14053  seqf1olem2a  14056  seqf1o  14059  ser1const  14074  expadd  14120  expmul  14123  leexp1a  14191  faccl  14299  facdiv  14303  faclbnd  14306  faclbnd4lem4  14312  hasheqf1oi  14367  hashgadd  14393  hashinfxadd  14401  hashunx  14402  hashunsng  14408  elprchashprn2  14412  hashss  14425  hash1snb  14435  hashmap  14451  hashf1lem2  14472  hashf1  14473  seqcoll  14480  hashle2pr  14493  hashdmpropge2  14499  hashge3el3dif  14503  hash1to3  14508  fundmge2nop0  14518  fi1uzind  14523  brfi1indALT  14526  sswrd  14538  swrdnd2  14671  swrdnnn0nd  14672  swrdnd0  14673  swrdwrdsymb  14678  pfxnd0  14704  swrdswrdlem  14720  swrdswrd  14721  wrd2ind  14739  swrdccatin1  14741  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccat3  14750  repsdf2  14794  repswswrd  14800  cshw0  14810  cshwcl  14814  cshwlen  14815  cshf1  14826  swrdco  14854  relexpsucnnl  15047  rtrclreclem3  15077  rtrclreclem4  15078  relexpindlem  15080  rtrclind  15082  shftlem  15085  caubnd  15375  reusq0  15479  rlimcld2  15592  o1dif  15644  climub  15676  climserle  15677  iseraltlem2  15697  sumss  15738  fsumzcl2  15753  fsummsnunz  15768  fsumsplitsnun  15769  fsum2d  15785  modfsummods  15807  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  climcndslem1  15863  climcndslem2  15864  cvgrat  15897  clim2prod  15902  prodfn0  15908  prodfrec  15909  ntrivcvg  15911  prodmo  15950  fprodss  15962  fprodabs  15988  fprodn0  15993  fprod2d  15995  fprodefsum  16109  ruclem8  16253  ruclem9  16254  dvdsmod0  16276  dvds2ln  16306  dvdsaddre2b  16324  dvdslelem  16326  dvdsdivcl  16333  alzdvds  16337  mod2eq1n2dvds  16364  oddnn02np1  16365  nn0o1gt2  16398  nno  16399  sumeven  16404  sumodd  16405  pwp1fsum  16408  ndvdsadd  16427  bitsinv1  16459  sadcadd  16475  sadadd2  16477  saddisjlem  16481  smuval2  16499  smupvallem  16500  smu01lem  16502  smupval  16505  smueqlem  16507  smumullem  16509  gcddiv  16568  rplpwr  16575  nn0seqcvgd  16587  seq1st  16588  alginv  16592  algcvga  16596  algfx  16597  absprodnn  16635  isprm2  16699  isprm3  16700  prmind2  16702  maxprmfct  16726  prmdvdsexp  16732  pcmpt  16910  prmreclem4  16937  vdwmc2  16997  vdwlem10  17008  ramub2  17032  ramcl  17047  prmgaplem5  17073  prmgaplem8  17076  cshwshashlem1  17113  cshwshashlem3  17115  setsn0fun  17190  imasleval  17553  divsfval  17559  mreexexlem4d  17657  isssc  17831  initoeu1  18022  termoeu1  18029  istos  18426  mgmcl  18619  sgrpidmnd  18715  frmdgsum  18838  smndex1mgm  18883  dfgrp3lem  19019  mhmmulg  19096  resghm2b  19215  gsumwrev  19347  elsymgbas  19353  symgextf1  19400  gsmsymgreqlem2  19410  gsmsymgreq  19411  odlem1  19514  odcl2  19544  gexlem1  19558  efgi2  19704  efginvrel2  19706  efgsrel  19713  cyggexb  19878  gsummulglem  19920  gsumzunsnd  19935  gsum2dlem2  19950  telgsums  19972  dmdprd  19979  dprdw  19991  ablfac1eulem  20053  srgpcomp  20176  rnghmmul  20407  nrhmzr  20495  lmodfopnelem1  20853  rmodislmodlem  20884  cnfldmulg  21364  cnfldexp  21365  nzerooringczr  21439  obslbs  21688  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  cply1mul  22232  coe1fzgsumdlem  22239  gsummoncoe1  22244  pf1ind  22291  evl1gsumdlem  22292  mat1dimcrng  22413  ma1repveval  22507  mulmarep1gsum2  22510  gsummatr01lem3  22593  cramerlem3  22625  decpmatmulsumfsupp  22709  mp2pm2mplem4  22745  pm2mpmhmlem1  22754  fvmptnn04if  22785  cayhamlem1  22802  fctop  22940  mretopd  23028  restopnb  23111  restdis  23114  tgcnp  23189  cncls2  23209  cncls  23210  cnntr  23211  cnsscnp  23215  cmpsub  23336  2ndcsep  23395  1stcelcls  23397  lfinpfin  23460  locfincmp  23462  comppfsc  23468  txcn  23562  txlm  23584  xkohaus  23589  qtopres  23634  haushmphlem  23723  cmphmph  23724  connhmph  23725  reghmph  23729  nrmhmph  23730  ptcmpfi  23749  reghaus  23761  fbssfi  23773  fbun  23776  fbfinnfr  23777  isfildlem  23793  fgcl  23814  cfinfil  23829  supfil  23831  ufinffr  23865  fin1aufil  23868  cnpflf  23937  alexsubALTlem3  23985  alexsubALT  23987  cnextfvval  24001  cnextcn  24003  tmdgsum  24031  tgphaus  24053  tgpt1  24054  mettri  24289  blssexps  24363  blssex  24364  mopni3  24431  metss  24445  psmetutop  24504  dscmet  24509  tngngp3  24593  rectbntr0  24770  metnrmlem1a  24796  fsumcn  24810  lmmbr  25208  caubl  25258  caublcls  25259  bcthlem5  25278  bcth3  25281  ovolunlem1a  25447  ovoliunnul  25458  finiunmbl  25495  voliunlem1  25501  volsuplem  25506  volsup  25507  dyadmax  25549  itgfsum  25778  dvnadd  25881  cpnord  25887  dvnfre  25906  dvmptfsum  25929  dvlip  25948  fta1g  26125  plyco  26196  dgrcolem1  26229  dgrco  26231  dvnply2  26245  plydivex  26255  plyexmo  26271  aannenlem1  26286  aaliou3lem2  26301  dvntaylp  26329  taylthlem1  26331  ulmval  26339  cxpmul2  26648  cxpsqrtth  26689  scvxcvx  26946  jensenlem2  26948  jensen  26949  ppiub  27165  bcmono  27238  bpos1lem  27243  bposlem5  27249  gausslemma2dlem6  27333  lgsquad2lem2  27346  2lgslem3  27365  2lgs  27368  2sqnn  27400  addsqnreup  27404  2sqreultblem  27409  2sqreunnltblem  27412  dchrisumlem1  27450  dchrisum0flb  27471  pntpbnd1  27547  pntlemf  27566  qabvle  27586  qabvexp  27587  ostthlem2  27589  ostth2lem2  27595  sltval2  27618  sltsolem1  27637  negsprop  27984  mulsuniflem  28092  precsexlem6  28153  precsexlem7  28154  noseqind  28215  om2noseqlt  28222  n0addscl  28264  n0mulscl  28265  expsne0  28331  axeuclidlem  28887  axcontlem12  28900  umgrnloopv  29031  uhgredgrnv  29055  edglnl  29068  numedglnl  29069  usgruspgrb  29108  usgrnloopvALT  29126  usgredg2vlem2  29151  subupgr  29212  nbumgr  29272  uhgrnbgr0nb  29279  nbgr0edglem  29281  edgusgrnbfin  29298  nb3grprlem2  29306  uvtxnbgrvtx  29318  cplgrop  29362  cusgrfi  29384  fusgrmaxsize  29390  fusgrn0degnn0  29425  ewlkprop  29529  uspgr2wlkeq  29572  g0wlk0  29578  wlkreslem  29595  lfgriswlk  29614  upgrwlkdvde  29665  spthonepeq  29680  uhgrwkspth  29683  usgr2trlncl  29688  usgr2trlspth  29689  cyclnumvtx  29728  cyclnspth  29729  crctcshwlkn0lem3  29740  wwlksn  29765  wspthneq1eq2  29788  wwlksm1edg  29809  wwlksnred  29820  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextproplem3  29839  wspthsnonn0vne  29845  wspn0  29852  rusgrnumwwlk  29903  clwwlkccatlem  29916  umgrclwwlkge2  29918  clwlkclwwlklem2  29927  clwlkclwwlklem3  29928  clwwisshclwws  29942  clwwisshclwwsn  29943  clwwlkn1loopb  29970  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  clwwlknonex2lem2  30035  upgr3v3e3cycl  30107  uhgr3cyclex  30109  upgr4cycl4dv4e  30112  eupth2lem3lem4  30158  eupth2lem3lem7  30161  eupth2  30166  eulerpath  30168  nfrgr2v  30199  frgr3vlem1  30200  3vfriswmgr  30205  1to2vfriswmgr  30206  1to3vfriswmgr  30207  3cyclfrgrrn1  30212  3cyclfrgrrn  30213  3cyclfrgrrn2  30214  4cycl2vnunb  30217  frgrncvvdeqlem2  30227  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  frgrwopreglem4a  30237  frgrwopreglem5lem  30247  frgrwopreglem5ALT  30249  frgrregorufr0  30251  frgr2wwlk1  30256  frgr2wwlkeqm  30258  fusgr2wsp2nb  30261  2wspmdisj  30264  frrusgrord  30268  numclwwlk1lem2f1  30284  numclwlk1  30298  frgrreggt1  30320  friendshipgt3  30325  hlim2  31119  elnlfn  31855  stle0i  32166  hstrbi  32193  spansncv2  32220  h1da  32276  fmptcof2  32581  sgn3da  32759  xreceu  32842  domnprodn0  33216  1arithufdlem3  33507  1arithufdlem4  33508  tpr2rico  33889  hasheuni  34062  ismeas  34176  sseqp1  34373  rrvsum  34432  dstfrvunirn  34453  signstfvc  34552  bnj607  34893  bnj1145  34970  bnj1204  34989  fineqvrep  35072  fisshasheq  35083  subgrwlk  35100  subfacp1lem6  35153  cvmlift2lem12  35282  cvmlift3lem4  35290  satfrnmapom  35338  sat1el2xp  35347  satffunlem2  35376  satffun  35377  mrsubvrs  35490  climuzcnv  35639  iprodefisumlem  35703  dfon2lem9  35755  linethru  36117  elhf2  36139  finminlem  36282  fnessref  36321  neibastop2lem  36324  fnemeet2  36331  nndivsub  36421  bj-xpnzex  36923  bj-elpwg  37016  bj-epelg  37032  mptsnunlem  37302  dissneqlem  37304  topdifinffinlem  37311  iooelexlt  37326  domalom  37368  fvineqsneq  37376  wl-exeq  37498  wl-ax11-lem3  37551  matunitlindflem1  37586  poimirlem22  37612  poimirlem26  37616  poimirlem28  37618  poimirlem29  37619  poimirlem32  37622  heicant  37625  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  cover2  37685  upixp  37699  sdclem2  37712  fdc  37715  seqpo  37717  metf1o  37725  mettrifi  37727  sstotbnd3  37746  heibor1lem  37779  heiborlem5  37785  heibor  37791  bfplem1  37792  elghomlem2OLD  37856  grpokerinj  37863  isrngo  37867  rngodm1dm2  37902  ispridl2  38008  exlimddvf  38091  lssatle  38979  4atexlemex4  40038  uzindd  41936  evl1gprodd  42076  sn-axprlem3  42214  redvmptabs  42350  sn-sup3d  42462  mzpsubst  42718  jm2.18  42959  wepwsolem  43013  oaabsb  43265  oacl2g  43301  ofoafg  43325  ofoaid1  43329  ofoaid2  43330  naddonnn  43366  iunrelexp0  43673  relexpmulg  43681  cnvtrclfv  43695  clsk1indlem3  44014  grucollcld  44232  inaex  44269  dvgrat  44284  radcnvrat  44286  csbxpgVD  44866  sineq0ALT  44909  trfr  44935  relwf  44940  pwclaxpow  44957  omssaxinf2  44961  islptre  45596  iblspltprt  45950  stoweidlem2  45979  stoweidlem17  45994  stoweidlem21  45998  2reuimp0  47091  2reuimp  47092  afveu  47130  funbrafv  47135  ndmaovass  47183  afv2eu  47215  tz6.12c-afv2  47219  funop1  47260  f1oresf1o2  47268  fvmptrabdm  47270  nltle2tri  47290  2elfz2melfz  47295  fsummsndifre  47334  fsumsplitsndif  47335  fsummmodsndifre  47336  fsummmodsnunz  47337  elsetpreimafvssdm  47348  uniimaelsetpreimafv  47358  imasetpreimafvbijlemfv1  47365  iccpartiltu  47384  iccpartigtl  47385  iccpartleu  47390  iccpartgel  47391  iccpartrn  47392  iccpartiun  47396  icceuelpart  47398  iccpartnel  47400  fargshiftf  47402  fargshiftf1  47403  ichnfb  47427  elsprel  47437  prsprel  47449  sprsymrelfo  47459  paireqne  47473  sbcpr  47483  reupr  47484  fmtnoinf  47498  odz2prm2pw  47525  lighneallem4  47572  lighneal  47573  requad1  47584  requad2  47585  evensumeven  47669  even3prm2  47681  gbowgt5  47724  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbnnsum3prm  47766  bgoldbtbndlem2  47768  bgoldbtbndlem4  47770  bgoldbtbnd  47771  dfsclnbgr6  47819  grimco  47850  cycl3grtri  47907  isubgr3stgrlem6  47931  gricgrlic  47971  gpgedgvtx0  48013  gpgprismgr4cycllem3  48044  clcllaw  48114  rngccatidALTV  48195  ringccatidALTV  48229  scmsuppss  48294  gsumlsscl  48303  ply1mulgsumlem2  48311  lincvalsc0  48345  linc0scn0  48347  lincdifsn  48348  linc1  48349  lincellss  48350  lincsum  48353  lincscm  48354  lincsumcl  48355  lcoss  48360  lincext3  48380  lindslinindimp2lem4  48385  lindslinindsimp2lem5  48386  lindslinindsimp2  48387  lindsrng01  48392  snlindsntor  48395  lincresunit3lem2  48404  lincresunit3  48405  islindeps2  48407  blengt1fldiv2p1  48521  2arymaptf1  48581  resum2sqorgt0  48637  reorelicc  48638  rrx2plordisom  48651  rrx2linest  48670  rrxsphere  48676  line2ylem  48679  itsclc0xyqsol  48696  itscnhlinecirc02p  48713  mo0sn  48742  thincn0eu  49265