Theorem expcom 404

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  ancoms  452  pm3.21  465  sylan  575  syldan  585  animpimp2impd  835  4casesdan  1025  dedlema  1029  dedlemb  1030  cbval2  2374  cbvaldva  2376  2moswap  2674  2eu2  2682  pm2.61ne  3055  nelelne  3070  r19.21be  3115  rspcebdv  3516  minel  4258  uneqdifeq  4281  raltpd  4547  ssunsn2  4591  opthprneg  4630  ssuni  4697  uniss2  4707  elpwuni  4852  disjord  4877  elssabg  5055  elpw2g  5063  oteqex  5197  otsndisj  5218  otiunsndisj  5219  epelg  5269  wereu  5353  relop  5520  riinint  5630  sotri3  5783  unixpid  5926  ordtr2  6022  ordsssuc2  6066  funopg  6171  fun  6318  tz6.12c  6473  fvmptnf  6565  fvn0ssdmfun  6616  eldmrexrnb  6632  fmptco  6663  fnressn  6693  fressnfv  6695  fprb  6733  fvtp2g  6738  fvtp3g  6739  fconst2g  6742  fntpb  6747  f1dom3el3dif  6800  isores3  6859  isoselem  6865  oprabv  6982  eloprabga  7026  sorpsscmpl  7227  difex2  7248  ordpwsuc  7295  ordsucun  7305  limuni3  7332  ordom  7354  fo1stres  7473  poxp  7572  soxp  7573  suppimacnv  7589  frnsuppeq  7590  funsssuppss  7605  brtpos2  7642  wfrlem12  7711  onnseq  7726  smores  7734  smofvon2  7738  tfrlem1  7757  oacl  7901  omcl  7902  oecl  7903  oawordri  7916  oalimcl  7926  oaass  7927  oarec  7928  omwordri  7938  omeulem1  7948  omeulem2  7949  oeordi  7953  oeworde  7959  oeoelem  7964  nnacl  7977  nnmcl  7978  nnecl  7979  nnacom  7983  nnaass  7988  nnmsucr  7991  nnmordi  7997  omabs  8013  iiner  8104  elpmg  8158  pmss12g  8169  mapfvd  8179  f1domg  8263  ssdomg  8289  domtriord  8396  php  8434  php3  8436  1sdom  8453  fisseneq  8461  isinf  8463  ssnnfi  8469  dif1en  8483  findcard3  8493  frfi  8495  unfi  8517  difinf  8520  fnfi  8528  iunfi  8544  fsuppunfi  8585  fsuppres  8590  frnfsuppbi  8594  elfi2  8610  marypha1lem  8629  marypha1  8630  oiexg  8731  wemapso2  8749  harword  8761  brwdom  8763  unxpwdom  8785  en3lplem1  8806  inf3lemd  8823  inf3lem5  8828  cantnfval2  8865  cantnfle  8867  cantnflt  8868  cnfcom  8896  tcmin  8916  r1sdom  8936  rankxplim3  9043  cardidm  9120  cardmin2  9159  infxpenlem  9171  fseqenlem1  9182  numacn  9207  alephordi  9232  iscard3  9251  alephinit  9253  carduniima  9254  iunfictbso  9272  dfac5  9286  dfac12lem3  9304  pwsdompw  9363  pwcdadom  9375  cflim2  9422  cfslb2n  9427  cofsmo  9428  cfsmolem  9429  cfcoflem  9431  alephsing  9435  infpssALT  9472  fin23lem34  9505  isf32lem2  9513  isf32lem10  9521  isf32lem12  9523  isfin1-2  9544  hsmexlem4  9588  axcc2lem  9595  domtriomlem  9601  axdc2lem  9607  axdc3lem2  9610  axdc3lem4  9612  axdc4lem  9614  axcclem  9616  ac6num  9638  ac6s  9643  zorn2lem7  9661  ttukeylem5  9672  imadomg  9693  iundom2g  9699  ondomon  9722  ficard  9724  konigthlem  9727  alephreg  9741  pwcfsdom  9742  cfpwsdom  9743  axregndlem1  9761  axregnd  9763  pwfseqlem3  9819  pwxpndom2  9824  pwxpndom  9825  pwcdandom  9826  inawinalem  9848  gchina  9858  wuncval2  9906  tsk0  9922  tskxpss  9931  inatsk  9937  tskuni  9942  gruina  9977  grothac  9989  addclpi  10051  addnidpi  10060  nqereu  10088  mulcanenq  10119  genpnnp  10164  nqpr  10173  prlem934  10192  reclem2pr  10207  suplem1pr  10211  supsrlem  10270  axpre-sup  10328  1re  10378  dedekindle  10542  00id  10553  receu  11023  sup3  11339  infrelb  11367  peano5nni  11382  nnaddcl  11403  zrevaddcl  11779  nzadd  11782  zdiv  11804  nneo  11818  zeo2  11821  nn0indd  11831  fzind  11832  fnn0ind  11833  uzwo  12063  lbzbi  12088  nn01to3  12093  qrevaddcl  12123  irradd  12125  irrmul  12126  ltsubrp  12180  ltaddrp  12181  xnn0xaddcl  12383  xnn0xadd0  12394  icoshft  12614  fzen  12680  elfzm11  12734  uzsplit  12735  elfzoext  12849  elfzom1elp1fzo  12859  injresinjlem  12912  injresinj  12913  modifeq2int  13056  modsumfzodifsn  13067  om2uzlti  13073  ssnn0fi  13108  fsuppmapnn0fiub0  13116  mptnn0fsuppr  13122  seqcaopr3  13159  seqf1olem2a  13162  seqf1o  13165  ser1const  13180  expadd  13225  expmul  13228  leexp1a  13242  faccl  13394  facdiv  13398  faclbnd  13401  faclbnd4lem4  13407  hasheqf1oi  13463  hashgadd  13487  hashinfxadd  13495  hashunx  13496  hashunsng  13502  elprchashprn2  13504  hashss  13517  hash1snb  13527  hashmap  13542  hashf1lem2  13560  hashf1  13561  seqcoll  13568  hashle2pr  13579  hashdmpropge2  13585  hashge3el3dif  13588  hash1to3  13593  fundmge2nop0  13594  fi1uzind  13599  brfi1indALT  13602  sswrd  13613  swrdnd2  13756  swrdnnn0nd  13757  swrdnd0  13758  swrdwrdsymb  13772  pfxnd0  13803  swrdswrdlem  13819  swrdswrd  13820  wrd2ind  13850  wrd2indOLD  13851  swrdccatin1  13857  swrdccatin2  13862  pfxccatin12lem2  13864  swrdccatin12lem2OLD  13865  pfxccat3  13869  swrdccat3OLD  13870  repsdf2  13930  repswswrd  13936  cshw0  13951  cshwcl  13955  cshwlen  13956  cshf1  13967  swrdco  13994  relexpsucnnl  14185  rtrclreclem3  14213  rtrclreclem4  14214  relexpindlem  14216  rtrclind  14218  shftlem  14221  caubnd  14512  rlimcld2  14726  o1dif  14777  climub  14809  climserle  14810  iseraltlem2  14830  sumss  14871  fsumzcl2  14885  fsummsnunz  14899  fsumsplitsnun  14900  fsum2d  14916  modfsummods  14938  fsumabs  14946  fsumrlim  14956  fsumo1  14957  fsumiun  14966  climcndslem1  14994  climcndslem2  14995  cvgrat  15027  clim2prod  15032  prodfn0  15038  prodfrec  15039  ntrivcvg  15041  prodmo  15078  fprodss  15090  fprodabs  15116  fprodn0  15121  fprod2d  15123  fprodefsum  15236  ruclem8  15379  ruclem9  15380  dvdsmod0  15402  dvds2ln  15431  dvdsaddre2b  15446  dvdslelem  15448  dvdsdivcl  15455  alzdvds  15459  mod2eq1n2dvds  15485  oddnn02np1  15486  nn0o1gt2  15521  nno  15522  sumeven  15527  sumodd  15528  pwp1fsum  15531  ndvdsadd  15550  bitsinv1  15580  sadcadd  15596  sadadd2  15598  saddisjlem  15602  smuval2  15620  smupvallem  15621  smu01lem  15623  smupval  15626  smueqlem  15628  smumullem  15630  gcddiv  15684  gcdmultiple  15685  rplpwr  15692  nn0seqcvgd  15699  seq1st  15700  alginv  15704  algcvga  15708  algfx  15709  absprodnn  15747  isprm2  15811  isprm3  15812  prmind2  15814  maxprmfct  15836  prmdvdsexp  15842  pcmpt  16011  prmreclem4  16038  vdwmc2  16098  vdwlem10  16109  ramub2  16133  ramcl  16148  prmgaplem5  16174  prmgaplem8  16177  cshwshashlem1  16212  cshwshashlem3  16214  setsn0fun  16303  imasleval  16598  divsfval  16604  mreexexlem4d  16704  isssc  16876  initoeu1  17057  termoeu1  17064  istos  17432  mgmcl  17642  frmdgsum  17797  dfgrp3lem  17911  mhmmulg  17978  resghm2b  18073  gsumwrev  18190  elsymgbas  18196  symgextf1  18235  gsmsymgreqlem2  18245  gsmsymgreq  18246  odlem1  18349  odcl2  18377  gexlem1  18389  efgi2  18533  efginvrel2  18535  efgsrel  18542  cyggexb  18697  gsummulglem  18738  gsumzunsnd  18752  gsum2dlem2  18767  telgsums  18788  dmdprd  18795  dprdw  18807  ablfac1eulem  18869  srgpcomp  18930  lmodfopnelem1  19302  rmodislmodlem  19333  mplcoe1  19873  mplcoe3  19874  mplcoe5  19876  cply1mul  20071  coe1fzgsumdlem  20078  gsummoncoe1  20081  pf1ind  20126  evl1gsumdlem  20127  cnfldmulg  20185  cnfldexp  20186  obslbs  20484  mat1dimcrng  20699  ma1repveval  20793  mulmarep1gsum2  20796  gsummatr01lem3  20880  cramerlem3  20913  decpmatmulsumfsupp  20996  mp2pm2mplem4  21032  pm2mpmhmlem1  21041  fvmptnn04if  21072  cayhamlem1  21089  fctop  21227  mretopd  21315  restopnb  21398  restdis  21401  tgcnp  21476  cncls2  21496  cncls  21497  cnntr  21498  cnsscnp  21502  cmpsub  21623  2ndcsep  21682  1stcelcls  21684  lfinpfin  21747  locfincmp  21749  comppfsc  21755  txcn  21849  txlm  21871  xkohaus  21876  qtopres  21921  haushmphlem  22010  cmphmph  22011  connhmph  22012  reghmph  22016  nrmhmph  22017  ptcmpfi  22036  reghaus  22048  fbssfi  22060  fbun  22063  fbfinnfr  22064  isfildlem  22080  fgcl  22101  cfinfil  22116  supfil  22118  ufinffr  22152  fin1aufil  22155  cnpflf  22224  alexsubALTlem3  22272  alexsubALT  22274  cnextfvval  22288  cnextcn  22290  tmdgsum  22318  tgphaus  22339  tgpt1  22340  mettri  22576  blssexps  22650  blssex  22651  mopni3  22718  metss  22732  psmetutop  22791  dscmet  22796  tngngp3  22879  rectbntr0  23054  metnrmlem1a  23080  fsumcn  23092  lmmbr  23475  caubl  23525  caublcls  23526  bcthlem5  23545  bcth3  23548  ovolunlem1a  23711  ovoliunnul  23722  finiunmbl  23759  voliunlem1  23765  volsuplem  23770  volsup  23771  dyadmax  23813  itgfsum  24041  dvnadd  24140  cpnord  24146  dvnfre  24163  dvmptfsum  24186  dvlip  24204  fta1g  24375  plyco  24445  dgrcolem1  24477  dgrco  24479  dvnply2  24490  plydivex  24500  plyexmo  24516  aannenlem1  24531  aaliou3lem2  24546  dvntaylp  24573  taylthlem1  24575  ulmval  24582  cxpmul2  24883  cxpsqrtth  24923  scvxcvx  25175  jensenlem2  25177  jensen  25178  ppiub  25392  bcmono  25465  bpos1lem  25470  bposlem5  25476  gausslemma2dlem6  25560  lgsquad2lem2  25573  2lgslem3  25592  2lgs  25595  dchrisumlem1  25647  dchrisum0flb  25668  pntpbnd1  25744  pntlemf  25763  qabvle  25783  qabvexp  25784  ostthlem2  25786  ostth2lem2  25792  axeuclidlem  26328  axcontlem12  26341  umgrnloopv  26471  uhgredgrnv  26495  edglnl  26509  numedglnl  26510  usgruspgrb  26547  usgrnloopvALT  26564  usgredg2vlem2  26589  subupgr  26651  nbumgr  26711  uhgrnbgr0nb  26718  nbgr0vtxlem  26719  edgusgrnbfin  26738  nb3grprlem2  26746  uvtxnbgrvtx  26758  cplgrop  26802  cusgrfi  26823  fusgrmaxsize  26829  fusgrn0degnn0  26864  ewlkprop  26968  uspgr2wlkeq  27010  g0wlk0  27016  wlkreslem  27035  wlkreslemOLD  27037  wlkresOLD  27038  lfgriswlk  27056  upgrwlkdvde  27106  spthonepeq  27121  uhgrwkspth  27124  usgr2trlncl  27129  usgr2trlspth  27130  cyclnspth  27169  crctcshwlkn0lem3  27178  wwlksn  27203  wspthneq1eq2  27226  wwlksm1edg  27247  wwlksm1edgOLD  27248  wwlksnred  27269  wwlksnredOLD  27270  wwlksnextfun  27279  wwlksnextinj  27280  wwlksnextfunOLD  27284  wwlksnextinjOLD  27285  wwlksnextproplem3  27304  wwlksnextproplem3OLD  27305  wspthsnonn0vne  27314  wspn0  27321  rusgrnumwwlk  27373  clwwlkccatlem  27386  umgrclwwlkge2  27388  clwlkclwwlklem2  27397  clwlkclwwlklem3  27398  clwwisshclwws  27421  clwwisshclwwsn  27422  clwwlkn1loopb  27450  clwwlknfiOLD  27453  wwlksext2clwwlk  27471  wwlksubclwwlk  27472  wwlksubclwwlkOLD  27473  clwwlknonwwlknonb  27525  clwwlknonex2lem2  27527  upgr3v3e3cycl  27600  uhgr3cyclex  27602  upgr4cycl4dv4e  27605  eupthseg  27626  upgreupthseg  27629  eupth2lem3lem4  27652  eupth2lem3lem7  27655  eupth2  27660  eulerpath  27662  nfrgr2v  27697  frgr3vlem1  27698  3vfriswmgr  27703  1to2vfriswmgr  27704  1to3vfriswmgr  27705  3cyclfrgrrn1  27710  3cyclfrgrrn  27711  3cyclfrgrrn2  27712  4cycl2vnunb  27715  frgrncvvdeqlem2  27725  frgrncvvdeqlem8  27731  frgrncvvdeqlem9  27732  frgrwopreglem4a  27735  frgrwopreglem5lem  27745  frgrwopreglem5ALT  27747  frgrregorufr0  27749  frgr2wwlk1  27754  frgr2wwlkeqm  27756  fusgr2wsp2nb  27759  2wspmdisj  27762  frrusgrord  27766  numclwwlk1lem2f1  27790  numclwwlk1lem2f1OLD  27795  numclwlk1  27816  frgrreggt1  27842  friendshipgt3  27847  hlim2  28638  elnlfn  29376  stle0i  29687  hstrbi  29714  spansncv2  29741  h1da  29797  fmptcof2  30039  nnindd  30144  xreceu  30206  tpr2rico  30564  hasheuni  30753  ismeas  30868  sseqp1  31064  rrvsum  31123  dstfrvunirn  31143  sgn3da  31210  bnj607  31593  bnj1145  31668  bnj1204  31687  subfacp1lem6  31774  cvmlift2lem12  31903  cvmlift3lem4  31911  mrsubvrs  32026  climuzcnv  32170  iprodefisumlem  32228  dfon2lem9  32292  trpredtr  32326  trpredmintr  32327  dftrpred3g  32329  trpredrec  32334  soseq  32351  sltval2  32406  sltsolem1  32423  linethru  32857  elhf2  32879  finminlem  32909  fnessref  32948  neibastop2lem  32951  fnemeet2  32958  nndivsub  33047  bj-cbval2v  33330  bj-xpnzex  33526  bj-intss  33634  mptsnunlem  33788  dissneqlem  33790  topdifinffinlem  33797  iooelexlt  33812  wl-exeq  33922  wl-ax11-lem3  33965  matunitlindflem1  34040  poimirlem22  34066  poimirlem26  34070  poimirlem28  34072  poimirlem29  34073  poimirlem32  34076  heicant  34079  ovoliunnfl  34086  voliunnfl  34088  volsupnfl  34089  cover2  34142  upixp  34158  sdclem2  34171  fdc  34174  seqpo  34176  metf1o  34184  mettrifi  34186  sstotbnd3  34208  heibor1lem  34241  heiborlem5  34247  heibor  34253  bfplem1  34254  elghomlem2OLD  34318  grpokerinj  34325  isrngo  34329  rngodm1dm2  34364  ispridl2  34470  exlimddvf  34557  lssatle  35178  4atexlemex4  36236  mzpsubst  38285  jm2.18  38528  wepwsolem  38585  iunrelexp0  38965  relexpmulg  38973  cnvtrclfv  38987  clsk1indlem3  39311  dvgrat  39481  radcnvrat  39483  csbxpgVD  40077  sineq0ALT  40120  islptre  40773  iblspltprt  41130  stoweidlem2  41160  stoweidlem17  41175  stoweidlem21  41179  2reu2  42162  2reuimp0  42169  2reuimp  42170  afveu  42208  funbrafv  42213  ndmaovass  42261  afv2eu  42293  tz6.12c-afv2  42297  funop1  42338  f1oresf1o2  42346  fvmptrabdm  42348  nltle2tri  42369  2elfz2melfz  42374  fzoopth  42383  fsummsndifre  42388  fsumsplitsndif  42389  fsummmodsndifre  42390  fsummmodsnunz  42391  iccpartimp  42399  iccpartiltu  42404  iccpartigtl  42405  iccpartleu  42410  iccpartgel  42411  iccpartrn  42412  iccpartiun  42416  icceuelpart  42418  iccpartnel  42420  fargshiftf  42422  fargshiftf1  42423  elsprel  42428  prsprel  42440  sprsymrelfo  42450  paireqne  42464  fmtnoinf  42483  odz2prm2pw  42510  lighneallem4  42562  lighneal  42563  requad1  42574  requad2  42575  evensumeven  42655  even3prm2  42667  gbowgt5  42689  nnsum4primeseven  42727  nnsum4primesevenALTV  42728  bgoldbnnsum3prm  42731  bgoldbtbndlem2  42733  bgoldbtbndlem4  42735  bgoldbtbnd  42736  isomuspgrlem1  42754  clcllaw  42856  nrhmzr  42902  rnghmmul  42929  rngccatidALTV  43018  ringccatidALTV  43081  nzerooringczr  43101  scmsuppss  43182  gsumlsscl  43193  ply1mulgsumlem2  43204  lincvalsc0  43239  linc0scn0  43241  lincdifsn  43242  linc1  43243  lincellss  43244  lincsum  43247  lincscm  43248  lincsumcl  43249  lcoss  43254  lincext3  43274  lindslinindimp2lem4  43279  lindslinindsimp2lem5  43280  lindslinindsimp2  43281  lindsrng01  43286  snlindsntor  43289  lincresunit3lem2  43298  lincresunit3  43299  islindeps2  43301  blengt1fldiv2p1  43416  resum2sqorgt0  43459  reorelicc  43460  rrx2plordisom  43473  rrx2linest  43492  rrxsphere  43498  line2ylem  43501  itsclc0xyqsol  43518  itscnhlinecirc02p  43535