Theorem expcom 450

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ancoms  468  syldan  486  sylan  487  4casesdan  988  dedlema  993  dedlemb  994  19.40bOLD  1805  cbval2  2267  cbvaldva  2269  2moswap  2535  2eu2  2542  pm2.61ne  2867  nelelne  2880  r19.21be  2917  minel  3985  uneqdifeq  4009  uneqdifeqOLD  4010  raltpd  4258  ssunsn2  4299  ssuni  4395  ssuniOLD  4396  uniss2  4406  elpwuni  4549  elssabg  4746  elpw2g  4754  oteqex  4889  otsndisj  4904  otiunsndisj  4905  epelg  4950  wereu  5034  relop  5194  riinint  5303  sotri3  5445  unixpid  5587  ordtr2  5685  ordsssuc2  5731  funopg  5836  fun  5979  tz6.12c  6123  fvmptnf  6210  fvn0ssdmfun  6258  eldmrexrnb  6274  fmptco  6303  funopsn  6319  fnressn  6330  fressnfv  6332  fvtp2g  6369  fvtp3g  6370  fconst2g  6373  fntpb  6378  f1dom3el3dif  6426  isores3  6485  isoselem  6491  oprabv  6601  eloprabga  6645  sorpsscmpl  6846  difex2  6863  ordpwsuc  6907  ordsucun  6917  limuni3  6944  ordom  6966  fo1stres  7083  poxp  7176  soxp  7177  suppimacnv  7193  frnsuppeq  7194  funsssuppss  7208  brtpos2  7245  wfrlem12  7313  onnseq  7328  smores  7336  smofvon2  7340  tfrlem1  7359  oacl  7502  omcl  7503  oecl  7504  oawordri  7517  oalimcl  7527  oaass  7528  oarec  7529  omwordri  7539  omeulem1  7549  omeulem2  7550  oeordi  7554  oeworde  7560  oeoelem  7565  nnacl  7578  nnmcl  7579  nnecl  7580  nnacom  7584  nnaass  7589  nnmsucr  7592  nnmordi  7598  omabs  7614  iiner  7706  elpmg  7759  pmss12g  7770  mapsn  7785  f1domg  7861  ssdomg  7887  domtriord  7991  php  8029  php3  8031  1sdom  8048  fisseneq  8056  isinf  8058  ssnnfi  8064  dif1en  8078  findcard3  8088  frfi  8090  unfi  8112  difinf  8115  fnfi  8123  iunfi  8137  fsuppunfi  8178  fsuppres  8183  frnfsuppbi  8187  elfi2  8203  marypha1lem  8222  marypha1  8223  oiexg  8323  wemapso2  8341  harword  8353  brwdom  8355  unxpwdom  8377  en3lplem1  8394  inf3lemd  8407  inf3lem5  8412  cantnfval2  8449  cantnfle  8451  cantnflt  8452  cnfcom  8480  tcmin  8500  r1sdom  8520  rankxplim3  8627  cardidm  8668  cardmin2  8707  infxpenlem  8719  fseqenlem1  8730  numacn  8755  alephordi  8780  iscard3  8799  alephinit  8801  carduniima  8802  iunfictbso  8820  dfac5  8834  dfac12lem3  8850  pwsdompw  8909  pwcdadom  8921  cflim2  8968  cfslb2n  8973  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  alephsing  8981  infpssALT  9018  fin23lem34  9051  isf32lem2  9059  isf32lem10  9067  isf32lem12  9069  isfin1-2  9090  hsmexlem4  9134  axcc2lem  9141  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  ac6num  9184  ac6s  9189  zorn2lem7  9207  ttukeylem5  9218  imadomg  9237  iundom2g  9241  ondomon  9264  ficard  9266  konigthlem  9269  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  axregndlem1  9303  axregnd  9305  pwfseqlem3  9361  pwxpndom2  9366  pwxpndom  9367  pwcdandom  9368  inawinalem  9390  gchina  9400  wuncval2  9448  tsk0  9464  tskxpss  9473  inatsk  9479  tskuni  9484  gruina  9519  grothac  9531  addclpi  9593  addnidpi  9602  nqereu  9630  mulcanenq  9661  genpnnp  9706  nqpr  9715  prlem934  9734  reclem2pr  9749  suplem1pr  9753  supsrlem  9811  axpre-sup  9869  1re  9918  dedekindle  10080  00id  10090  receu  10551  sup3  10859  infrelb  10885  peano5nni  10900  nnaddcl  10919  zrevaddcl  11299  nzadd  11302  zdiv  11323  nneo  11337  zeo2  11340  nn0indd  11350  fzind  11351  fnn0ind  11352  uzwo  11627  lbzbi  11652  nn01to3  11657  qrevaddcl  11686  irradd  11688  irrmul  11689  ltsubrp  11742  ltaddrp  11743  xnn0xaddcl  11940  xnn0xadd0  11949  icoshft  12165  fzen  12229  elfzm11  12280  uzsplit  12281  elfzoext  12392  elfzom1elp1fzo  12402  injresinjlem  12450  injresinj  12451  modifeq2int  12594  modsumfzodifsn  12605  om2uzlti  12611  ssnn0fi  12646  fsuppmapnn0fiub0  12655  mptnn0fsuppr  12661  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqcaopr3  12698  seqf1olem2a  12701  seqf1o  12704  seqid2  12709  seqhomo  12710  ser1const  12719  expadd  12764  expmul  12767  leexp1a  12781  faccl  12932  facdiv  12936  faclbnd  12939  faclbnd4lem4  12945  faclbnd6  12948  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashf1rnOLD  13005  hashgadd  13027  hashinfxadd  13035  hashunx  13036  hashunsng  13042  elprchashprn2  13045  hashss  13058  hash1snb  13068  hashmap  13082  hashf1lem2  13097  hashf1  13098  seqcoll  13105  hashge2el2dif  13117  hashge3el3dif  13122  hash1to3  13128  fundmge2nop0  13129  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  sswrd  13168  swrdnd2  13285  swrdswrdlem  13311  swrdswrd  13312  wrd2ind  13329  swrdccatin1  13334  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccat3  13343  repsdf2  13376  repswswrd  13382  cshw0  13391  cshwcl  13395  cshwlen  13396  cshf1  13407  swrdco  13434  relexpsucnnl  13620  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  rtrclind  13653  shftlem  13656  caubnd  13946  rlimcld2  14157  o1dif  14208  climub  14240  climserle  14241  iseraltlem2  14261  sumss  14302  fsumzcl2  14316  fsummsnunz  14327  fsumsplitsnun  14328  fsum2d  14344  modfsummods  14366  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  cvgrat  14454  clim2prod  14459  prodfn0  14465  prodfrec  14466  ntrivcvg  14468  prodmo  14505  fprodss  14517  fprodabs  14543  fprodn0  14548  fprod2d  14550  fprodefsum  14664  ruclem8  14805  ruclem9  14806  dvds2ln  14852  dvdsaddre2b  14867  dvdslelem  14869  dvdsdivcl  14876  alzdvds  14880  mod2eq1n2dvds  14909  oddnn02np1  14910  nn0o1gt2  14935  nno  14936  sumeven  14948  sumodd  14949  pwp1fsum  14952  ndvdsadd  14972  bitsinv1  15002  sadcadd  15018  sadadd2  15020  saddisjlem  15024  smuval2  15042  smupvallem  15043  smu01lem  15045  smupval  15048  smueqlem  15050  smumullem  15052  gcddiv  15106  gcdmultiple  15107  rplpwr  15114  nn0seqcvgd  15121  seq1st  15122  alginv  15126  algcvga  15130  algfx  15131  absprodnn  15169  isprm2  15233  isprm3  15234  prmind2  15236  maxprmfct  15259  prmdvdsexp  15265  pcmpt  15434  prmreclem4  15461  vdwmc2  15521  vdwlem10  15532  ramub2  15556  ramcl  15571  prmgaplem5  15597  prmgaplem8  15600  cshwshashlem1  15640  cshwshashlem3  15642  imasleval  16024  divsfval  16030  mreexexlem4d  16130  isssc  16303  initoeu1  16484  termoeu1  16491  istos  16858  mgmcl  17068  frmdgsum  17222  dfgrp3lem  17336  mhmmulg  17406  resghm2b  17501  gsumwrev  17619  elsymgbas  17625  symgextf1  17664  gsmsymgreqlem2  17674  gsmsymgreq  17675  odlem1  17777  odcl2  17805  gexlem1  17817  sylow1lem1  17836  efgi2  17961  efginvrel2  17963  efgsrel  17970  cyggexb  18123  gsummulglem  18164  gsumzunsnd  18178  gsum2dlem2  18193  telgsums  18213  dmdprd  18220  dprdw  18232  ablfac1eulem  18294  srgpcomp  18355  lmodfopnelem1  18722  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  cply1mul  19485  coe1fzgsumdlem  19492  gsummoncoe1  19495  pf1ind  19540  evl1gsumdlem  19541  cnfldmulg  19597  cnfldexp  19598  obslbs  19893  mat1dimcrng  20102  ma1repveval  20196  mulmarep1gsum2  20199  gsummatr01lem3  20282  cramerlem3  20314  decpmatmulsumfsupp  20397  mp2pm2mplem4  20433  pm2mpmhmlem1  20442  fvmptnn04if  20473  cayhamlem1  20490  fctop  20618  mretopd  20706  restopnb  20789  restdis  20792  tgcnp  20867  cncls2  20887  cncls  20888  cnntr  20889  cnsscnp  20893  cmpsub  21013  2ndcsep  21072  1stcelcls  21074  lfinpfin  21137  locfincmp  21139  comppfsc  21145  txcn  21239  txlm  21261  xkohaus  21266  qtopres  21311  haushmphlem  21400  cmphmph  21401  conhmph  21402  reghmph  21406  nrmhmph  21407  ptcmpfi  21426  reghaus  21438  fbssfi  21451  fbun  21454  fbfinnfr  21455  isfildlem  21471  fgcl  21492  cfinfil  21507  supfil  21509  ufinffr  21543  fin1aufil  21546  cnpflf  21615  alexsubALTlem3  21663  alexsubALT  21665  cnextfvval  21679  cnextcn  21681  tmdmulg  21706  tmdgsum  21709  tgphaus  21730  tgpt1  21731  mettri  21967  imasdsf1olem  21988  blssexps  22041  blssex  22042  mopni3  22109  metss  22123  psmetutop  22182  dscmet  22187  tngngp3  22270  rectbntr0  22443  metnrmlem1a  22469  fsumcn  22481  lmmbr  22864  caubl  22914  caublcls  22915  bcthlem5  22933  bcth3  22936  ovolunlem1a  23071  ovoliunnul  23082  ovolicc2lem3  23094  finiunmbl  23119  voliunlem1  23125  volsuplem  23130  volsup  23131  dyadmax  23172  itgfsum  23399  dvnadd  23498  dvnres  23500  cpnord  23504  dvnfre  23521  dvmptfsum  23542  dvlip  23560  fta1g  23731  plyco  23801  dgrcolem1  23833  dgrco  23835  dvnply2  23846  plydivex  23856  plyexmo  23872  aannenlem1  23887  aaliou3lem2  23902  dvntaylp  23929  taylthlem1  23931  ulmval  23938  cxpmul2  24235  scvxcvx  24512  jensenlem2  24514  jensen  24515  ppiub  24729  bcmono  24802  bpos1lem  24807  bposlem5  24813  gausslemma2dlem6  24897  lgsquad2lem2  24910  2lgslem3  24929  2lgs  24932  dchrisumlem1  24978  dchrisum0flb  24999  pntpbnd1  25075  pntlemf  25094  qabvle  25114  qabvexp  25115  ostthlem2  25117  ostth2lem2  25123  axeuclidlem  25642  axcontlem12  25655  uhgrstrrepelem  25744  umgrnloopv  25772  uhgredgrnv  25804  usgraedgprv  25905  usgranloopv  25907  usgraidx2vlem2  25921  usgrafisbase  25943  edgusgranbfin  25979  nb3graprlem2  25981  cusgra2v  25991  cusgrafi  26010  sizeusglecusglem1  26012  sizeusglecusg  26014  usgramaxsize  26015  iswlkg  26052  2trllemH  26082  2trllemE  26083  usgrwlknloop  26093  spthonepeq  26117  wlkdvspthlem  26137  wlkdvspth  26138  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  cyclnspth  26159  fargshiftf  26164  fargshiftf1  26165  3v3e3cycl2  26192  3v3e3cycl  26193  4cycl4dv  26195  wwlkn0  26217  usg2wlkeq  26236  wwlknred  26251  wwlkextfun  26257  wwlkextinj  26258  wwlkm1edg  26263  wwlkextproplem3  26271  clwwlkgt0  26299  clwlkisclwwlklem1  26315  clwlkisclwwlklem0  26316  wwlksubclwwlk  26332  clwwisshclww  26335  clwwisshclwwn  26336  clwlkfclwwlk  26371  2wlkonot3v  26402  2spthonot3v  26403  usg2wlkonot  26410  usg2wotspth  26411  usgfidegfi  26437  cusgraisrusgra  26465  rusgranumwlk  26484  iseupa  26492  eupatrl  26495  eupath2  26507  frgra2v  26526  frgra3vlem1  26527  3vfriswmgra  26532  1to2vfriswmgra  26533  1to3vfriswmgra  26534  2pthfrgra  26538  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  3cyclfrgrarn2  26541  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  frgrancvvdeqlem4  26560  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgrawopreglem2  26572  frgrawopreglem4  26574  frgrawopreg  26576  frgraregorufr0  26579  frgraeu  26581  frg2woteqm  26586  2spotmdisj  26595  usgreghash2spot  26596  clwwlkextfrlem1  26603  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwlk1lem2f1  26621  frgrareg  26644  friendshipgt3  26648  hlim2  27433  elnlfn  28171  stle0i  28482  hstrbi  28509  spansncv2  28536  h1da  28592  fmptcof2  28839  nnindd  28953  xreceu  28961  tpr2rico  29286  hasheuni  29474  ismeas  29589  sseqp1  29784  rrvsum  29843  dstfrvunirn  29863  sgn3da  29930  bnj607  30240  bnj1145  30315  bnj1204  30334  subfacp1lem6  30421  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem12  30550  cvmlift3lem4  30558  mrsubvrs  30673  climuzcnv  30819  iprodefisumlem  30879  fprb  30916  dfon2lem9  30940  trpredtr  30974  trpredmintr  30975  dftrpred3g  30977  trpredrec  30982  soseq  30995  frrlem11  31036  sltval2  31053  sltsolem1  31067  linethru  31430  elhf2  31452  finminlem  31482  fnessref  31522  neibastop2lem  31525  fnemeet2  31532  nndivsub  31626  bj-cbval2v  31924  bj-xpnzex  32139  mptsnunlem  32361  dissneqlem  32363  topdifinffinlem  32371  iooelexlt  32386  wl-exeq  32500  wl-ax11-lem3  32543  matunitlindflem1  32575  poimirlem22  32601  poimirlem26  32605  poimirlem28  32607  poimirlem29  32608  poimirlem32  32611  heicant  32614  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  cover2  32678  upixp  32694  sdclem2  32708  fdc  32711  seqpo  32713  metf1o  32721  mettrifi  32723  sstotbnd3  32745  heibor1lem  32778  heiborlem5  32784  heibor  32790  bfplem1  32791  elghomlem2OLD  32855  grpokerinj  32862  isrngo  32866  rngodm1dm2  32901  ispridl2  33007  exlimddvf  33096  lssatle  33320  4atexlemex4  34377  mzpsubst  36329  jm2.18  36573  wepwsolem  36630  iunrelexp0  37013  relexpmulg  37021  cnvtrclfv  37035  clsk1indlem3  37361  dvgrat  37533  radcnvrat  37535  sbcoreleleqVD  38117  csbxpgVD  38152  sineq0ALT  38195  islptre  38686  iblspltprt  38865  stoweidlem2  38895  stoweidlem17  38910  stoweidlem21  38914  2reu2  39836  afveu  39882  funbrafv  39887  ndmaovass  39935  nltle2tri  39942  smonoord  39944  iccpartimp  39955  iccpartiltu  39960  iccpartigtl  39961  iccpartleu  39966  iccpartgel  39967  iccpartrn  39968  iccpartiun  39972  icceuelpart  39974  iccpartnel  39976  fmtnoinf  39986  odz2prm2pw  40013  lighneallem4  40065  lighneal  40066  evensumeven  40154  gbogt5  40184  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxccatin12lem2  40287  pfxccat3  40289  funop1  40327  2elfz2melfz  40355  fzoopth  40360  fsummsndifre  40371  fsumsplitsndif  40372  fsummmodsndifre  40373  fsummmodsnunz  40374  usgruspgrb  40411  usgrnloopvALT  40428  usgredg2vlem2  40453  subupgr  40511  nbumgr  40569  uhgrnbgr0nb  40576  nbgr0vtxlem  40577  edgusgrnbfin  40601  nb3grprlem2  40609  uvtxanbgrvtx  40619  cplgrop  40659  cusgrfi  40674  fusgrmaxsize  40680  fusgrn0degnn0  40714  ewlkprop  40805  upgrwlkedg  40850  uspgr2wlkeq  40854  g01wlk0  40860  1wlkreslem  40878  1wlkres  40879  lfgriswlk  40897  upgrwlkdvde  40943  spthonepeq-av  40958  uhgr1wlkspth  40961  usgr2trlncl  40966  usgr2trlspth  40967  cyclnsPth  41006  crctcsh1wlkn0lem3  41015  wwlksn  41040  wspthneq1eq2  41056  wwlksm1edg  41078  wwlksnred  41098  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextproplem3  41117  wspthsnonn0vne  41124  rusgrnumwwlk  41178  clwwlksn  41189  clwlkclwwlklem2  41209  clwlkclwwlklem3  41210  umgrclwwlksge2  41219  wwlksubclwwlks  41232  clwwisshclwws  41235  clwwisshclwwsn  41236  clwlksfclwwlk  41269  upgr3v3e3cycl  41347  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  eupthseg  41374  upgreupthi  41376  upgreupthseg  41377  eupth2lem3lem4  41399  eupth2lem3lem7  41402  eupth2  41407  eulerpath  41409  nfrgr2v  41442  frgr3vlem1  41443  3vfriswmgr  41448  1to2vfriswmgr  41449  1to3vfriswmgr  41450  3cyclfrgrrn1  41455  3cyclfrgrrn  41456  3cyclfrgrrn2  41457  4cycl2vnunb-av  41460  frgrncvvdeqlem4  41472  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  frgrwopreglem4  41484  frgrwopreg  41486  frgrregorufr0  41489  frgreu  41491  frgr2wwlk1  41494  fusgr2wsp2nb  41498  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwlk1lem2f1  41524  av-frgrareggt1  41547  av-friendshipgt3  41552  clcllaw  41617  nrhmzr  41663  rnghmmul  41690  rngccatidALTV  41781  ringccatidALTV  41844  nzerooringczr  41864  scmsuppss  41947  gsumlsscl  41958  ply1mulgsumlem2  41969  lincvalsc0  42004  linc0scn0  42006  lincdifsn  42007  linc1  42008  lincellss  42009  lincsum  42012  lincscm  42013  lincsumcl  42014  lcoss  42019  lincext3  42039  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lindsrng01  42051  snlindsntor  42054  lincresunit3lem2  42063  lincresunit3  42064  islindeps2  42066  blengt1fldiv2p1  42185