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  2132  mo4  2591  2moswapv  2654  2moswap  2669  2eu2  2677  pm2.61ne  3040  nelelne  3056  r19.21be  3255  rspcebdv  3570  2reu2  3846  csbie2df  4401  minel  4419  uneqdifeq  4448  raltpd  4742  ssunsn2  4788  opthprneg  4825  ssuni  4893  uniss2  4902  elpwuni  5065  intss2  5068  disjord  5092  elpw2g  5298  elssabg  5307  axprlem3OLD  5394  axprlem4OLD  5395  axprlem5OLD  5396  axprglem  5401  oteqex  5477  otsndisj  5496  otiunsndisj  5497  epelg  5556  wereu  5651  relop  5830  riinint  5956  sotri3  6124  unixpid  6282  reuop  6291  ordtr2  6403  ordsssuc2  6451  iotan0  6523  funopg  6568  fun  6738  fvmptnf  7010  fvn0ssdmfun  7068  eldmrexrnb  7086  fmptco  7124  fnressn  7156  fressnfv  7158  fprb  7193  fvtp2g  7198  fvtp3g  7199  fconst2g  7203  fntpb  7209  f1dom3el3dif  7267  f1ounsn  7274  isores3  7337  isoselem  7343  oprabv  7474  eloprabga  7523  sorpsscmpl  7736  difex2  7760  ordpwsuc  7812  ordsucun  7822  limuni3  7849  trom  7872  fo1stres  8013  poxp  8127  soxp  8128  xpord3inddlem  8153  soseq  8158  suppimacnv  8173  fsuppeq  8174  funsssuppss  8189  brtpos2  8231  frrlem8  8293  fpr2a  8302  onnseq  8334  smores  8342  smofvon2  8346  tfrlem1  8365  oacl  8523  omcl  8524  oecl  8525  oawordri  8538  oalimcl  8548  oaass  8549  oarec  8550  omwordri  8560  omeulem1  8570  omeulem2  8571  oeordi  8576  oeworde  8582  oeoelem  8587  nnacl  8600  nnmcl  8601  nnecl  8602  nnacom  8606  nnaass  8611  nnmsucr  8614  nnmordi  8620  omabs  8640  cofonr  8663  naddunif  8683  iiner  8790  elpmg  8843  fsetfcdm  8862  fsetprcnex  8864  pmss12g  8877  mapfvd  8887  f1domg  8978  ssdomg  9007  undom  9064  domtriord  9122  ssnnfi  9165  fnfi  9173  enfi  9182  php  9202  sdom1  9221  1sdom2dom  9225  fisseneq  9234  isinf  9236  dif1ennnALT  9248  findcard3  9254  frfi  9256  difinf  9282  iunfi  9311  fsuppunfi  9359  fsuppres  9364  ffsuppbi  9369  elfi2  9385  marypha1lem  9404  marypha1  9405  oiexg  9508  wemapso2  9526  harword  9536  brwdom  9540  unxpwdom  9562  en3lplem1  9592  inf3lemd  9607  inf3lem5  9612  cantnfval2  9649  cantnfle  9651  cantnflt  9652  cnfcom  9680  tcmin  9719  frr2  9743  r1sdom  9757  rankxplim3  9864  cardidm  9965  cardmin2  10005  infxpenlem  10017  fseqenlem1  10028  numacn  10053  alephordi  10078  iscard3  10097  alephinit  10099  carduniima  10100  iunfictbso  10118  dfac5  10132  dfac12lem3  10149  nnadju  10201  pwsdompw  10206  pwdjudom  10218  cflim2  10266  cfslb2n  10271  cofsmo  10272  cfsmolem  10273  cfcoflem  10275  alephsing  10279  infpssALT  10316  fin23lem34  10349  isf32lem2  10357  isf32lem10  10365  isf32lem12  10367  isfin1-2  10388  hsmexlem4  10432  axcc2lem  10439  domtriomlem  10445  axdc2lem  10451  axdc3lem2  10454  axdc3lem4  10456  axdc4lem  10458  axcclem  10460  ac6num  10482  ac6s  10487  zorn2lem7  10505  ttukeylem5  10516  imadomg  10538  iundom2g  10549  ondomon  10572  ficard  10574  konigthlem  10578  alephreg  10592  pwcfsdom  10593  cfpwsdom  10594  axregndlem1  10612  axregnd  10614  pwfseqlem3  10670  pwxpndom2  10675  pwxpndom  10676  pwdjundom  10677  inawinalem  10699  gchina  10709  wuncval2  10757  tsk0  10773  tskxpss  10782  inatsk  10788  tskuni  10793  gruina  10828  grothac  10840  addclpi  10902  addnidpi  10911  nqereu  10939  mulcanenq  10970  genpnnp  11015  nqpr  11024  prlem934  11043  reclem2pr  11058  suplem1pr  11062  supsrlem  11121  axpre-sup  11179  1re  11233  dedekindle  11399  00id  11410  receu  11884  sup3  12197  infrelb  12225  peano5nni  12261  nnindd  12278  nnaddcl  12281  zrevaddcl  12664  nzadd  12667  zdiv  12692  nneo  12706  zeo2  12709  nn0indd  12719  fzind  12720  fnn0ind  12721  fzindd  12724  uzwo  12961  lbzbi  12986  nn01to3  12991  qrevaddcl  13022  irradd  13024  irrmul  13025  ltsubrp  13081  ltaddrp  13082  xnn0xaddcl  13288  xnn0xadd0  13300  icoshft  13527  fzen  13596  elfzm11  13651  uzsplit  13652  elfzom1elp1fzo  13789  fzoopth  13819  injresinjlem  13847  injresinj  13848  modifeq2int  13998  modsumfzodifsn  14009  om2uzlti  14015  ssnn0fi  14050  fsuppmapnn0fiub0  14058  mptnn0fsuppr  14064  seqcaopr3  14102  seqf1olem2a  14105  seqf1o  14108  ser1const  14123  expadd  14169  expmul  14172  leexp1a  14240  faccl  14348  facdiv  14352  faclbnd  14355  faclbnd4lem4  14361  hasheqf1oi  14416  hashgadd  14442  hashinfxadd  14450  hashunx  14451  hashunsng  14457  elprchashprn2  14461  hashss  14474  hash1snb  14485  hashmap  14501  hashf1lem2  14522  hashf1  14523  seqcoll  14530  hashle2pr  14543  hashdmpropge2  14549  hashge3el3dif  14553  hash1to3  14558  fundmge2nop0  14568  fi1uzind  14573  brfi1indALT  14576  sswrd  14588  swrdnd2  14726  swrdnnn0nd  14727  swrdnd0  14728  swrdwrdsymb  14733  pfxnd0  14759  swrdswrdlem  14774  swrdswrd  14775  wrd2ind  14793  swrdccatin1  14795  swrdccatin2  14799  pfxccatin12lem2  14801  pfxccat3  14804  repsdf2  14850  repswswrd  14856  cshw0  14866  cshwcl  14870  cshwlen  14871  cshf1  14882  swrdco  14909  relexpsucnnl  15104  rtrclreclem3  15134  rtrclreclem4  15135  relexpindlem  15137  rtrclind  15139  shftlem  15142  sgn3da  15175  caubnd  15447  reusq0  15553  rlimcld2  15666  o1dif  15718  climub  15750  climserle  15751  iseraltlem2  15771  sumss  15811  fsumzcl2  15826  fsummsnunz  15841  fsumsplitsnun  15842  fsum2d  15858  modfsummods  15881  fsumabs  15889  fsumrlim  15899  fsumo1  15900  fsumiun  15909  climcndslem1  15939  climcndslem2  15940  cvgrat  15973  clim2prod  15978  prodfn0  15984  prodfrec  15985  ntrivcvg  15987  prodmo  16024  fprodss  16036  fprodabs  16062  fprodn0  16067  fprod2d  16069  fprodefsum  16182  ruclem8  16326  ruclem9  16327  dvdsmod0  16349  dvds2ln  16380  dvdsaddre2b  16398  dvdslelem  16400  dvdsdivcl  16407  alzdvds  16411  mod2eq1n2dvds  16438  oddnn02np1  16439  nn0o1gt2  16472  nno  16473  sumeven  16478  sumodd  16479  pwp1fsum  16482  ndvdsadd  16501  bitsinv1  16533  sadcadd  16549  sadadd2  16551  saddisjlem  16555  smuval2  16573  smupvallem  16574  smu01lem  16576  smupval  16579  smueqlem  16581  smumullem  16583  gcddiv  16642  rplpwr  16649  nn0seqcvgd  16661  seq1st  16662  alginv  16666  algcvga  16670  algfx  16671  absprodnn  16709  isprm2  16773  isprm3  16774  prmind2  16776  maxprmfct  16801  prmdvdsexp  16807  pcmpt  16985  prmreclem4  17012  vdwmc2  17072  vdwlem10  17083  ramub2  17107  ramcl  17122  prmgaplem5  17148  prmgaplem8  17151  cshwshashlem1  17188  cshwshashlem3  17190  setsn0fun  17266  imasleval  17628  divsfval  17634  mreexexlem4d  17736  isssc  17910  initoeu1  18101  termoeu1  18108  istos  18505  chnfibg  18725  mgmcl  18734  sgrpidmnd  18842  frmdgsum  18972  smndex1mgm  19020  dfgrp3lem  19162  mhmmulg  19239  resghm2b  19362  gsumwrev  19494  elsymgbas  19502  symgextf1  19549  gsmsymgreqlem2  19559  gsmsymgreq  19560  odlem1  19663  odcl2  19693  gexlem1  19707  efgi2  19853  efginvrel2  19855  efgsrel  19862  cyggexb  20027  gsummulglem  20069  gsumzunsnd  20084  gsum2dlem2  20099  telgsums  20121  dmdprd  20128  dprdw  20140  ablfac1eulem  20202  srgpcomp  20358  rnghmmul  20591  nrhmzr  20700  lmodfopnelem1  21083  rmodislmodlem  21114  cnfldmulg  21618  cnfldexp  21619  nzerooringczr  21694  obslbs  21944  mplcoe1  22254  mplcoe3  22255  mplcoe5  22257  cply1mul  22522  coe1fzgsumdlem  22529  gsummoncoe1  22534  pf1ind  22581  evl1gsumdlem  22582  mat1dimcrng  22700  ma1repveval  22794  mulmarep1gsum2  22797  gsummatr01lem3  22880  matunitlindflem1  22902  cramerlem3  22915  decpmatmulsumfsupp  22999  mp2pm2mplem4  23035  pm2mpmhmlem1  23044  fvmptnn04if  23075  cayhamlem1  23092  fctop  23230  mretopd  23318  restopnb  23401  restdis  23404  tgcnp  23479  cncls2  23499  cncls  23500  cnntr  23501  cnsscnp  23505  cmpsub  23626  2ndcsep  23686  1stcelcls  23688  lfinpfin  23751  locfincmp  23753  comppfsc  23759  txcn  23853  txlm  23875  xkohaus  23880  qtopres  23925  haushmphlem  24014  cmphmph  24015  connhmph  24016  reghmph  24020  nrmhmph  24021  ptcmpfi  24040  reghaus  24052  fbssfi  24064  fbun  24067  fbfinnfr  24068  isfildlem  24084  fgcl  24105  cfinfil  24120  supfil  24122  ufinffr  24156  fin1aufil  24159  cnpflf  24228  alexsubALTlem3  24276  alexsubALT  24278  cnextfvval  24292  cnextcn  24294  tmdgsum  24322  tgphaus  24344  tgpt1  24345  mettri  24579  blssexps  24653  blssex  24654  mopni3  24721  metss  24735  psmetutop  24794  dscmet  24799  tngngp3  24883  rectbntr0  25060  metnrmlem1a  25086  fsumcn  25099  lmmbr  25487  caubl  25537  caublcls  25538  bcthlem5  25557  bcth3  25560  ovolunlem1a  25725  ovoliunnul  25736  finiunmbl  25773  voliunlem1  25779  volsuplem  25784  volsup  25785  dyadmax  25827  itgfsum  26055  dvnadd  26157  cpnord  26163  dvnfre  26180  dvmptfsum  26203  dvlip  26221  fta1g  26396  plyco  26468  dgrcolem1  26500  dgrco  26502  dvnply2  26518  plydivex  26528  plyexmo  26546  aannenlem1  26565  aaliou3lem2  26580  dvntaylp  26608  taylthlem1  26610  ulmval  26617  cxpmul2  26927  cxpsqrtth  26968  scvxcvx  27223  jensenlem2  27225  jensen  27226  ppiub  27441  bcmono  27514  bpos1lem  27519  bposlem5  27525  gausslemma2dlem6  27609  lgsquad2lem2  27622  2lgslem3  27641  2lgs  27644  2sqnn  27676  addsqnreup  27680  2sqreultblem  27685  2sqreunnltblem  27688  dchrisumlem1  27726  dchrisum0flb  27747  pntpbnd1  27823  pntlemf  27842  qabvle  27862  qabvexp  27863  ostthlem2  27865  ostth2lem2  27871  ltsval2  27893  ltssolem1  27912  negsprop  28301  mulsuniflem  28415  precsexlem6  28478  precsexlem7  28479  noseqind  28558  om2noseqlt  28565  n0addscl  28610  n0mulscl  28611  expsne0  28702  axeuclidlem  29420  axcontlem12  29433  umgrnloopv  29564  uhgredgrnv  29588  edglnl  29601  numedglnl  29602  usgruspgrb  29644  usgrnloopvALT  29662  usgredg2vlem2  29687  subupgr  29748  nbumgr  29808  uhgrnbgr0nb  29815  nbgr0edglem  29817  edgusgrnbfin  29834  nb3grprlem2  29842  uvtxnbgrvtx  29854  cplgrop  29898  cusgrfi  29919  fusgrmaxsize  29925  fusgrn0degnn0  29960  ewlkprop  30064  uspgr2wlkeq  30106  g0wlk0  30111  wlkreslem  30128  subgrwlk  30149  lfgriswlk  30151  upgrwlkdvde  30203  spthonepeq  30218  uhgrwkspth  30221  usgr2trlncl  30226  usgr2trlspth  30227  cyclnumvtx  30268  cyclnspth  30269  crctcshwlkn0lem3  30281  wwlksn  30306  wspthneq1eq2  30329  wwlksm1edg  30350  wwlksnred  30361  wwlksnextfun  30367  wwlksnextinj  30368  wwlksnextproplem3  30380  wspthsnonn0vne  30386  wspn0  30393  rusgrnumwwlk  30447  clwwlkccatlem  30460  umgrclwwlkge2  30462  clwlkclwwlklem2  30471  clwlkclwwlklem3  30472  clwwisshclwws  30486  clwwisshclwwsn  30487  clwwlkn1loopb  30514  wwlksext2clwwlk  30528  wwlksubclwwlk  30529  clwwlknonex2lem2  30579  upgr3v3e3cycl  30661  uhgr3cyclex  30663  upgr4cycl4dv4e  30666  eupth2lem3lem4  30712  eupth2lem3lem7  30715  eupth2  30720  eulerpath  30722  nfrgr2v  30753  frgr3vlem1  30754  3vfriswmgr  30759  1to2vfriswmgr  30760  1to3vfriswmgr  30761  3cyclfrgrrn1  30766  3cyclfrgrrn  30767  3cyclfrgrrn2  30768  4cycl2vnunb  30771  frgrncvvdeqlem2  30781  frgrncvvdeqlem8  30787  frgrncvvdeqlem9  30788  frgrwopreglem4a  30791  frgrwopreglem5lem  30801  frgrwopreglem5ALT  30803  frgrregorufr0  30805  frgr2wwlk1  30810  frgr2wwlkeqm  30812  fusgr2wsp2nb  30815  2wspmdisj  30818  frrusgrord  30822  numclwwlk1lem2f1  30838  numclwlk1  30852  frgrreggt1  30874  friendshipgt3  30879  hlim2  31674  elnlfn  32410  stle0i  32721  hstrbi  32748  spansncv2  32775  h1da  32831  fmptcof2  33131  xreceu  33368  domnprodn0  33719  1arithufdlem3  33957  1arithufdlem4  33958  tpr2rico  34423  hasheuni  34596  ismeas  34711  sseqp1  34907  rrvsum  34966  dstfrvunirn  34987  signstfvc  35083  bnj607  35426  bnj1145  35503  bnj1204  35522  r1filim  35613  fineqvrep  35641  fineqvnttrclselem1  35648  onvf1odlem4  35704  vonf1oonfo  35713  fisshasheq  35718  subfacp1lem6  35765  cvmlift2lem12  35894  cvmlift3lem4  35902  satfrnmapom  35950  sat1el2xp  35959  satffunlem2  35988  satffun  35989  mrsubvrs  36102  climuzcnv  36251  iprodefisumlem  36320  dfon2lem9  36369  linethru  36734  elhf2  36756  finminlem  36938  fnessref  36977  neibastop2lem  36980  fnemeet2  36987  nndivsub  37077  mh-inf3f1  37161  bj-cbvew  37373  bj-xpnzex  37704  bj-elpwg  37797  bj-epelg  37813  bj-axseprep  37820  mptsnunlem  38093  dissneqlem  38095  topdifinffinlem  38102  iooelexlt  38117  domalom  38159  fvineqsneq  38167  wl-exeq  38298  poimirlem22  38392  poimirlem26  38396  poimirlem28  38398  poimirlem29  38399  poimirlem32  38402  heicant  38405  ovoliunnfl  38412  voliunnfl  38414  volsupnfl  38415  cover2  38466  upixp  38480  sdclem2  38493  fdc  38496  seqpo  38498  metf1o  38506  mettrifi  38508  sstotbnd3  38527  heibor1lem  38560  heiborlem5  38566  heibor  38572  bfplem1  38573  elghomlem2OLD  38637  grpokerinj  38644  isrngo  38648  rngodm1dm2  38683  ispridl2  38789  exlimddvf  38870  lssatle  39889  4atexlemex4  40947  uzindd  42845  evl1gprodd  42984  sn-axprlem3  43089  redvmptabs  43236  sn-sup3d  43381  mzpsubst  43594  jm2.18  43830  wepwsolem  43884  oaabsb  44136  oacl2g  44172  ofoafg  44196  ofoaid1  44200  ofoaid2  44201  naddonnn  44237  iunrelexp0  44543  relexpmulg  44551  cnvtrclfv  44565  clsk1indlem3  44884  grucollcld  45085  inaex  45122  dvgrat  45137  radcnvrat  45139  csbxpgVD  45717  sineq0ALT  45760  trfr  45786  relwf  45791  pwclaxpow  45808  omssaxinf2  45812  islptre  46450  iblspltprt  46802  stoweidlem2  46831  stoweidlem17  46846  stoweidlem21  46850  2reuimp0  48003  2reuimp  48004  afveu  48042  funbrafv  48047  ndmaovass  48095  afv2eu  48127  tz6.12c-afv2  48131  funop1  48172  f1oresf1o2  48180  fvmptrabdm  48182  nltle2tri  48202  2elfz2melfz  48207  fsummsndifre  48269  fsumsplitsndif  48270  fsummmodsndifre  48271  fsummmodsnunz  48272  elsetpreimafvssdm  48287  uniimaelsetpreimafv  48297  imasetpreimafvbijlemfv1  48304  iccpartiltu  48323  iccpartigtl  48324  iccpartleu  48329  iccpartgel  48330  iccpartrn  48331  iccpartiun  48335  icceuelpart  48337  iccpartnel  48339  fargshiftf  48341  fargshiftf1  48342  ichnfb  48366  elsprel  48376  prsprel  48388  sprsymrelfo  48398  paireqne  48412  sbcpr  48422  reupr  48423  fmtnoinf  48440  odz2prm2pw  48467  lighneallem4  48514  lighneal  48515  requad1  48539  requad2  48540  evensumeven  48624  even3prm2  48636  gbowgt5  48679  nnsum4primeseven  48717  nnsum4primesevenALTV  48718  bgoldbnnsum3prm  48721  bgoldbtbndlem2  48723  bgoldbtbndlem4  48725  bgoldbtbnd  48726  dfsclnbgr6  48775  grimco  48806  cycl3grtri  48864  isubgr3stgrlem6  48888  gricgrlic  48935  gpgedgvtx0  48978  gpgprismgr4cycllem3  49014  pgnbgreunbgrlem5  49040  clcllaw  49107  rngccatidALTV  49188  ringccatidALTV  49222  scmsuppss  49302  gsumlsscl  49311  ply1mulgsumlem2  49318  lincvalsc0  49352  linc0scn0  49354  lincdifsn  49355  linc1  49356  lincellss  49357  lincsum  49360  lincscm  49361  lincsumcl  49362  lcoss  49367  lincext3  49387  lindslinindimp2lem4  49392  lindslinindsimp2lem5  49393  lindslinindsimp2  49394  lindsrng01  49399  snlindsntor  49402  lincresunit3lem2  49411  lincresunit3  49412  islindeps2  49414  blengt1fldiv2p1  49524  2arymaptf1  49584  resum2sqorgt0  49640  reorelicc  49641  rrx2plordisom  49654  rrx2linest  49673  rrxsphere  49679  line2ylem  49682  itsclc0xyqsol  49699  itscnhlinecirc02p  49716  mo0sn  49745  thincn0eu  50358  alsralrex  50742  alsraln0  50743