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  2131  mo4  2591  2moswapv  2654  2moswap  2669  2eu2  2677  pm2.61ne  3040  nelelne  3056  r19.21be  3255  rspcebdv  3570  2reu2  3845  csbie2df  4400  minel  4418  uneqdifeq  4447  raltpd  4738  ssunsn2  4782  opthprneg  4819  ssuni  4892  uniss2  4901  elpwuni  5064  intss2  5067  disjord  5091  elpw2g  5294  elssabg  5303  axprglem  5393  oteqex  5471  otsndisj  5491  otiunsndisj  5492  epelg  5551  wereu  5646  relop  5827  riinint  5953  sotri3  6123  unixpid  6287  reuop  6296  ordtr2  6408  ordsssuc2  6456  iotan0  6528  iotan0OLD  6529  funopg  6575  fun  6745  fvmptnf  7017  fvn0ssdmfun  7075  eldmrexrnb  7093  fmptco  7131  fnressn  7163  fressnfv  7165  fprb  7200  fvtp2g  7205  fvtp3g  7206  fconst2g  7210  fntpb  7216  f1dom3el3dif  7274  f1ounsn  7281  isores3  7344  isoselem  7350  oprabv  7481  eloprabga  7530  sorpsscmpl  7751  difex2  7775  ordpwsuc  7827  ordsucun  7837  limuni3  7864  trom  7887  fo1stres  8028  poxp  8143  soxp  8144  xpord3inddlem  8174  soseq  8179  suppimacnv  8195  fsuppeq  8196  funsssuppss  8211  brtpos2  8253  frrlem8  8315  fpr2a  8324  onnseq  8356  smores  8364  smofvon2  8368  tfrlem1  8387  oacl  8547  omcl  8548  oecl  8549  oawordri  8562  oalimcl  8572  oaass  8573  oarec  8574  omwordri  8584  omeulem1  8594  omeulem2  8595  oeordi  8600  oeworde  8606  oeoelem  8611  nnacl  8624  nnmcl  8625  nnecl  8626  nnacom  8630  nnaass  8635  nnmsucr  8638  nnmordi  8644  omabs  8664  cofonr  8687  naddunif  8707  iiner  8814  elpmg  8867  fsetfcdm  8886  fsetprcnex  8888  pmss12g  8901  mapfvd  8911  f1domg  9002  ssdomg  9031  undom  9088  domtriord  9146  ssnnfi  9189  fnfi  9197  enfi  9206  php  9226  sdom1  9245  1sdom2dom  9249  fisseneq  9258  isinf  9260  dif1ennnALT  9272  findcard3  9278  frfi  9280  difinf  9307  iunfi  9336  fsuppunfi  9384  fsuppres  9389  ffsuppbi  9394  elfi2  9410  marypha1lem  9429  marypha1  9430  oiexg  9533  wemapso2  9551  harword  9561  brwdom  9565  unxpwdom  9587  en3lplem1  9617  inf3lemd  9632  inf3lem5  9637  cantnfval2  9674  cantnfle  9676  cantnflt  9677  cnfcom  9705  tcmin  9744  frr2  9768  r1sdom  9785  rankxplim3  9902  elhf2  9914  elhf3OLD  9927  hfpw  9930  cardidm  10044  cardmin2  10084  infxpenlem  10096  fseqenlem1  10107  numacn  10132  alephordi  10157  iscard3  10176  alephinit  10178  carduniima  10179  iunfictbso  10197  dfac5  10211  dfac12lem3  10228  nnadju  10280  pwsdompw  10285  pwdjudom  10297  cflim2  10345  cfslb2n  10350  cofsmo  10351  cfsmolem  10352  cfcoflem  10354  alephsing  10358  infpssALT  10395  fin23lem34  10428  isf32lem2  10436  isf32lem10  10444  isf32lem12  10446  isfin1-2  10467  hsmexlem4  10511  axcc2lem  10518  domtriomlem  10524  axdc2lem  10530  axdc3lem2  10533  axdc3lem4  10535  axdc4lem  10537  axcclem  10539  ac6num  10561  ac6s  10566  zorn2lem7  10584  ttukeylem5  10595  imadomg  10617  iundom2g  10628  ondomon  10651  ficard  10653  konigthlem  10657  alephreg  10671  pwcfsdom  10672  cfpwsdom  10673  axregndlem1  10691  axregnd  10693  pwfseqlem3  10749  pwxpndom2  10754  pwxpndom  10755  pwdjundom  10756  inawinalem  10778  gchina  10788  wuncval2  10836  tsk0  10852  tskxpss  10861  inatsk  10867  tskuni  10872  gruina  10907  grothac  10919  addclpi  10981  addnidpi  10990  nqereu  11018  mulcanenq  11049  genpnnp  11094  nqpr  11103  prlem934  11122  reclem2pr  11137  suplem1pr  11141  supsrlem  11200  axpre-sup  11258  1re  11312  dedekindle  11478  00id  11489  receu  11965  sup3  12278  infrelb  12306  peano5nni  12342  nnindd  12359  nnaddcl  12362  zrevaddcl  12745  nzadd  12748  zdiv  12773  nneo  12787  zeo2  12790  nn0indd  12800  fzind  12801  fnn0ind  12802  fzindd  12805  uzwo  13042  lbzbi  13067  nn01to3  13072  qrevaddcl  13103  irradd  13105  irrmul  13106  ltsubrp  13162  ltaddrp  13163  xnn0xaddcl  13369  xnn0xadd0  13381  icoshft  13608  fzen  13678  elfzm11  13733  uzsplit  13734  elfzom1elp1fzo  13871  fzoopth  13901  injresinjlem  13929  injresinj  13930  modifeq2int  14080  modsumfzodifsn  14091  om2uzlti  14097  ssnn0fi  14132  fsuppmapnn0fiub0  14140  mptnn0fsuppr  14146  seqcaopr3  14184  seqf1olem2a  14187  seqf1o  14190  ser1const  14205  expadd  14251  expmul  14254  leexp1a  14322  faccl  14431  facdiv  14435  faclbnd  14438  faclbnd4lem4  14444  hasheqf1oi  14499  hashgadd  14525  hashinfxadd  14533  hashunx  14534  hashunsng  14540  elprchashprn2  14544  hashss  14557  hash1snb  14568  hashmap  14584  hashf1lem2  14605  hashf1  14606  seqcoll  14613  hashle2pr  14626  hashdmpropge2  14632  hashge3el3dif  14636  hash1to3  14641  fundmge2nop0  14651  fi1uzind  14656  brfi1indALT  14659  sswrd  14671  swrdnd2  14810  swrdnnn0nd  14811  swrdnd0  14812  swrdwrdsymb  14817  pfxnd0  14843  swrdswrdlem  14858  swrdswrd  14859  wrd2ind  14877  swrdccatin1  14879  swrdccatin2  14883  pfxccatin12lem2  14885  pfxccat3  14888  repsdf2  14934  repswswrd  14940  cshw0  14950  cshwcl  14954  cshwlen  14955  cshf1  14966  swrdco  14993  relexpsucnnl  15189  rtrclreclem3  15219  rtrclreclem4  15220  relexpindlem  15222  rtrclind  15224  shftlem  15227  sgn3da  15260  caubnd  15532  reusq0  15638  rlimcld2  15751  o1dif  15803  climub  15835  climserle  15836  iseraltlem2  15856  sumss  15896  fsumzcl2  15911  fsummsnunz  15926  fsumsplitsnun  15927  fsum2d  15943  modfsummods  15966  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  climcndslem1  16024  climcndslem2  16025  cvgrat  16058  clim2prod  16063  prodfn0  16069  prodfrec  16070  ntrivcvg  16072  prodmo  16109  fprodss  16121  fprodabs  16147  fprodn0  16152  fprod2d  16154  fprodefsum  16267  ruclem8  16411  ruclem9  16412  dvdsmod0  16434  dvds2ln  16465  dvdsaddre2b  16483  dvdslelem  16485  dvdsdivcl  16492  alzdvds  16496  mod2eq1n2dvds  16523  oddnn02np1  16524  nn0o1gt2  16557  nno  16558  sumeven  16563  sumodd  16564  pwp1fsum  16567  ndvdsadd  16586  bitsinv1  16618  sadcadd  16634  sadadd2  16636  saddisjlem  16640  smuval2  16658  smupvallem  16659  smu01lem  16661  smupval  16664  smueqlem  16666  smumullem  16668  gcddiv  16730  rplpwr  16738  nn0seqcvgd  16751  seq1st  16752  alginv  16756  algcvga  16760  algfx  16761  absprodnn  16799  isprm2  16863  isprm3  16864  prmind2  16866  maxprmfct  16891  prmdvdsexp  16897  pcmpt  17076  prmreclem4  17103  vdwmc2  17163  vdwlem10  17174  ramub2  17198  ramcl  17213  prmgaplem5  17239  prmgaplem8  17242  cshwshashlem1  17279  cshwshashlem3  17281  setsn0fun  17357  imasleval  17719  divsfval  17725  mreexexlem4d  17827  isssc  18001  initoeu1  18192  termoeu1  18199  istos  18596  chnfibg  18816  mgmcl  18825  frmdgsum  19064  smndex1mgm  19112  dfgrp3lem  19254  mhmmulg  19331  resghm2b  19454  gsumwrev  19586  elsymgbas  19594  symgextf1  19641  gsmsymgreqlem2  19651  gsmsymgreq  19652  odlem1  19755  odcl2  19785  gexlem1  19799  efgi2  19945  efginvrel2  19947  efgsrel  19954  cyggexb  20119  gsummulglem  20161  gsumzunsnd  20176  gsum2dlem2  20191  telgsums  20213  dmdprd  20220  dprdw  20232  ablfac1eulem  20294  srgpcomp  20450  rnghmmul  20685  nrhmzr  20795  lmodfopnelem1  21179  rmodislmodlem  21210  cnfldmulg  21716  cnfldexp  21717  nzerooringczr  21792  obslbs  22042  mplcoe1  22352  mplcoe3  22353  mplcoe5  22355  cply1mul  22620  coe1fzgsumdlem  22627  gsummoncoe1  22632  pf1ind  22679  evl1gsumdlem  22680  mat1dimcrng  22798  ma1repveval  22892  mulmarep1gsum2  22895  gsummatr01lem3  22978  matunitlindflem1  23000  cramerlem3  23013  decpmatmulsumfsupp  23097  mp2pm2mplem4  23133  pm2mpmhmlem1  23142  fvmptnn04if  23173  cayhamlem1  23190  fctop  23328  mretopd  23416  restopnb  23499  restdis  23502  tgcnp  23577  cncls2  23597  cncls  23598  cnntr  23599  cnsscnp  23603  cmpsub  23724  2ndcsep  23784  1stcelcls  23786  lfinpfin  23849  locfincmp  23851  comppfsc  23857  txcn  23951  txlm  23973  xkohaus  23978  qtopres  24023  haushmphlem  24112  cmphmph  24113  connhmph  24114  reghmph  24118  nrmhmph  24119  ptcmpfi  24138  reghaus  24150  fbssfi  24162  fbun  24165  fbfinnfr  24166  isfildlem  24182  fgcl  24203  cfinfil  24218  supfil  24220  ufinffr  24254  fin1aufil  24257  cnpflf  24326  alexsubALTlem3  24374  alexsubALT  24376  cnextfvval  24390  cnextcn  24392  tmdgsum  24420  tgphaus  24442  tgpt1  24443  mettri  24677  blssexps  24751  blssex  24752  mopni3  24819  metss  24833  psmetutop  24892  dscmet  24897  tngngp3  24981  rectbntr0  25158  metnrmlem1a  25184  fsumcn  25197  lmmbr  25585  caubl  25635  caublcls  25636  bcthlem5  25655  bcth3  25658  ovolunlem1a  25823  ovoliunnul  25834  finiunmbl  25871  voliunlem1  25877  volsuplem  25882  volsup  25883  dyadmax  25925  itgfsum  26153  dvnadd  26255  cpnord  26261  dvnfre  26278  dvmptfsum  26301  dvlip  26319  fta1g  26494  plyco  26566  dgrcolem1  26598  dgrco  26600  dvnply2  26614  plydivex  26624  plyexmo  26642  aannenlem1  26661  aaliou3lem2  26676  dvntaylp  26704  taylthlem1  26706  ulmval  26713  cxpmul2  27023  cxpsqrtth  27064  scvxcvx  27319  jensenlem2  27321  jensen  27322  ppiub  27537  bcmono  27610  bpos1lem  27615  bposlem5  27621  gausslemma2dlem6  27705  lgsquad2lem2  27718  2lgslem3  27737  2lgs  27740  2sqnn  27772  addsqnreup  27776  2sqreultblem  27781  2sqreunnltblem  27784  dchrisumlem1  27822  dchrisum0flb  27843  pntpbnd1  27919  pntlemf  27938  qabvle  27958  qabvexp  27959  ostthlem2  27961  ostth2lem2  27967  ltsval2  28019  ltssolem1  28038  negsprop  28427  mulsuniflem  28541  precsexlem6  28604  precsexlem7  28605  noseqind  28684  om2noseqlt  28691  n0addscl  28736  n0mulscl  28737  expsne0  28828  axeuclidlem  29546  axcontlem12  29559  umgrnloopv  29690  uhgredgrnv  29714  edglnl  29727  numedglnl  29728  usgruspgrb  29770  usgrnloopvALT  29788  usgredg2vlem2  29813  subupgr  29874  nbumgr  29934  uhgrnbgr0nb  29941  nbgr0edglem  29943  edgusgrnbfin  29960  nb3grprlem2  29968  uvtxnbgrvtx  29980  cplgrop  30024  cusgrfi  30045  fusgrmaxsize  30051  fusgrn0degnn0  30086  ewlkprop  30190  uspgr2wlkeq  30232  g0wlk0  30237  wlkreslem  30254  subgrwlk  30275  lfgriswlk  30277  upgrwlkdvde  30329  spthonepeq  30344  uhgrwkspth  30347  usgr2trlncl  30352  usgr2trlspth  30353  cyclnumvtx  30394  cyclnspth  30395  crctcshwlkn0lem3  30407  wwlksn  30432  wspthneq1eq2  30455  wwlksm1edg  30476  wwlksnred  30487  wwlksnextfun  30493  wwlksnextinj  30494  wwlksnextproplem3  30506  wspthsnonn0vne  30512  wspn0  30519  rusgrnumwwlk  30573  clwwlkccatlem  30586  umgrclwwlkge2  30588  clwlkclwwlklem2  30597  clwlkclwwlklem3  30598  clwwisshclwws  30612  clwwisshclwwsn  30613  clwwlkn1loopb  30640  wwlksext2clwwlk  30654  wwlksubclwwlk  30655  clwwlknonex2lem2  30705  upgr3v3e3cycl  30787  uhgr3cyclex  30789  upgr4cycl4dv4e  30792  eupth2lem3lem4  30838  eupth2lem3lem7  30841  eupth2  30846  eulerpath  30848  nfrgr2v  30879  frgr3vlem1  30880  3vfriswmgr  30885  1to2vfriswmgr  30886  1to3vfriswmgr  30887  3cyclfrgrrn1  30892  3cyclfrgrrn  30893  3cyclfrgrrn2  30894  4cycl2vnunb  30897  frgrncvvdeqlem2  30907  frgrncvvdeqlem8  30913  frgrncvvdeqlem9  30914  frgrwopreglem4a  30917  frgrwopreglem5lem  30927  frgrwopreglem5ALT  30929  frgrregorufr0  30931  frgr2wwlk1  30936  frgr2wwlkeqm  30938  fusgr2wsp2nb  30941  2wspmdisj  30944  frrusgrord  30948  numclwwlk1lem2f1  30964  numclwlk1  30978  frgrreggt1  31000  friendshipgt3  31005  hlim2  31800  elnlfn  32536  stle0i  32847  hstrbi  32874  spansncv2  32901  h1da  32957  fmptcof2  33299  xreceu  33535  domnprodn0  33886  1arithufdlem3  34125  1arithufdlem4  34126  tpr2rico  34591  hasheuni  34764  ismeas  34879  sseqp1  35074  rrvsum  35133  dstfrvunirn  35154  signstfvc  35250  bnj607  35593  bnj1145  35670  bnj1204  35689  dfac15  35810  dfac16  35811  acwer1prclem  35816  fineqvrep  35839  fineqvnttrclselem1  35846  j0ltaleph  35948  onvf1odlem4  35954  onprcf1acwevdlem1  35965  vonf1oonfo  35969  fisshasheq  35980  srepdflem2  36006  subfacp1lem6  36037  cvmlift2lem12  36166  cvmlift3lem4  36174  satfrnmapom  36222  sat1el2xp  36231  satffunlem2  36260  satffun  36261  mrsubvrs  36374  climuzcnv  36523  iprodefisumlem  36598  dfon2lem9  36646  linethru  37011  finminlem  37199  fnessref  37238  neibastop2lem  37241  fnemeet2  37248  nndivsub  37338  bj-cbvew  37634  bj-xpnzex  37965  bj-elpwg  38060  bj-epelg  38076  bj-axseprep  38083  mptsnunlem  38355  dissneqlem  38357  topdifinffinlem  38364  iooelexlt  38379  domalom  38421  fvineqsneq  38429  wl-exeq  38560  poimirlem22  38654  poimirlem26  38658  poimirlem28  38660  poimirlem29  38661  poimirlem32  38664  heicant  38667  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  cover2  38743  upixp  38757  sdclem2  38770  fdc  38773  seqpo  38775  metf1o  38783  mettrifi  38785  sstotbnd3  38804  heibor1lem  38837  heiborlem5  38843  heibor  38849  bfplem1  38850  elghomlem2OLD  38914  grpokerinj  38921  isrngo  38925  rngodm1dm2  38960  ispridl2  39066  exlimddvf  39147  lssatle  40166  4atexlemex4  41224  uzindd  43122  evl1gprodd  43261  sn-axprlem3  43366  redvmptabs  43505  sn-sup3d  43650  mzpsubst  43853  jm2.18  44089  wepwsolem  44143  oaabsb  44390  oacl2g  44426  ofoafg  44450  ofoaid1  44454  ofoaid2  44455  naddonnn  44491  iunrelexp0  44796  relexpmulg  44804  cnvtrclfv  44818  clsk1indlem3  45137  grucollcld  45338  inaex  45375  dvgrat  45390  radcnvrat  45392  csbxpgVD  45970  sineq0ALT  46013  trfr  46046  relwf  46051  pwclaxpow  46068  omssaxinf2  46072  islptre  46725  iblspltprt  47077  stoweidlem2  47106  stoweidlem17  47121  stoweidlem21  47125  2reuimp0  48278  2reuimp  48279  afveu  48317  funbrafv  48322  ndmaovass  48370  afv2eu  48402  tz6.12c-afv2  48406  funop1  48447  f1oresf1o2  48455  fvmptrabdm  48457  nltle2tri  48477  2elfz2melfz  48482  fsummsndifre  48544  fsumsplitsndif  48545  fsummmodsndifre  48546  fsummmodsnunz  48547  elsetpreimafvssdm  48562  uniimaelsetpreimafv  48572  imasetpreimafvbijlemfv1  48579  iccpartiltu  48598  iccpartigtl  48599  iccpartleu  48604  iccpartgel  48605  iccpartrn  48606  iccpartiun  48610  icceuelpart  48612  iccpartnel  48614  fargshiftf  48616  fargshiftf1  48617  ichnfb  48641  elsprel  48651  prsprel  48663  sprsymrelfo  48673  paireqne  48687  sbcpr  48697  reupr  48698  fmtnoinf  48715  odz2prm2pw  48742  lighneallem4  48789  lighneal  48790  requad1  48814  requad2  48815  evensumeven  48899  even3prm2  48911  gbowgt5  48954  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  bgoldbnnsum3prm  48996  bgoldbtbndlem2  48998  bgoldbtbndlem4  49000  bgoldbtbnd  49001  dfsclnbgr6  49050  grimco  49081  cycl3grtri  49139  isubgr3stgrlem6  49163  gricgrlic  49210  gpgedgvtx0  49253  gpgprismgr4cycllem3  49289  pgnbgreunbgrlem5  49315  clcllaw  49382  rngccatidALTV  49463  ringccatidALTV  49497  scmsuppss  49577  gsumlsscl  49586  ply1mulgsumlem2  49593  lincvalsc0  49627  linc0scn0  49629  lincdifsn  49630  linc1  49631  lincellss  49632  lincsum  49635  lincscm  49636  lincsumcl  49637  lcoss  49642  lincext3  49662  lindslinindimp2lem4  49667  lindslinindsimp2lem5  49668  lindslinindsimp2  49669  lindsrng01  49674  snlindsntor  49677  lincresunit3lem2  49686  lincresunit3  49687  islindeps2  49689  blengt1fldiv2p1  49799  2arymaptf1  49859  resum2sqorgt0  49915  reorelicc  49916  rrx2plordisom  49930  rrx2linest  49948  rrxsphere  49954  line2ylem  49957  itsclc0xyqsol  49974  itscnhlinecirc02p  49991  mo0sn  50021  thincn0eu  50660  alsralrex  51077  alsraln0  51078