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  6567  fun  6737  fvmptnf  7009  fvn0ssdmfun  7067  eldmrexrnb  7085  fmptco  7123  fnressn  7155  fressnfv  7157  fprb  7192  fvtp2g  7197  fvtp3g  7198  fconst2g  7202  fntpb  7208  f1dom3el3dif  7266  f1ounsn  7273  isores3  7336  isoselem  7342  oprabv  7473  eloprabga  7522  sorpsscmpl  7735  difex2  7759  ordpwsuc  7811  ordsucun  7821  limuni3  7848  trom  7871  fo1stres  8012  poxp  8126  soxp  8127  xpord3inddlem  8152  soseq  8157  suppimacnv  8172  fsuppeq  8173  funsssuppss  8188  brtpos2  8230  frrlem8  8292  fpr2a  8301  onnseq  8333  smores  8341  smofvon2  8345  tfrlem1  8364  oacl  8522  omcl  8523  oecl  8524  oawordri  8537  oalimcl  8547  oaass  8548  oarec  8549  omwordri  8559  omeulem1  8569  omeulem2  8570  oeordi  8575  oeworde  8581  oeoelem  8586  nnacl  8599  nnmcl  8600  nnecl  8601  nnacom  8605  nnaass  8610  nnmsucr  8613  nnmordi  8619  omabs  8639  cofonr  8662  naddunif  8682  iiner  8789  elpmg  8842  fsetfcdm  8861  fsetprcnex  8863  pmss12g  8876  mapfvd  8886  f1domg  8977  ssdomg  9006  undom  9063  domtriord  9121  ssnnfi  9164  fnfi  9172  enfi  9181  php  9201  sdom1  9220  1sdom2dom  9224  fisseneq  9233  isinf  9235  dif1ennnALT  9247  findcard3  9253  frfi  9255  difinf  9281  iunfi  9310  fsuppunfi  9358  fsuppres  9363  ffsuppbi  9368  elfi2  9384  marypha1lem  9403  marypha1  9404  oiexg  9507  wemapso2  9525  harword  9535  brwdom  9539  unxpwdom  9561  en3lplem1  9591  inf3lemd  9606  inf3lem5  9611  cantnfval2  9648  cantnfle  9650  cantnflt  9651  cnfcom  9679  tcmin  9718  frr2  9742  r1sdom  9756  rankxplim3  9863  cardidm  9964  cardmin2  10004  infxpenlem  10016  fseqenlem1  10027  numacn  10052  alephordi  10077  iscard3  10096  alephinit  10098  carduniima  10099  iunfictbso  10117  dfac5  10131  dfac12lem3  10148  nnadju  10200  pwsdompw  10205  pwdjudom  10217  cflim2  10265  cfslb2n  10270  cofsmo  10271  cfsmolem  10272  cfcoflem  10274  alephsing  10278  infpssALT  10315  fin23lem34  10348  isf32lem2  10356  isf32lem10  10364  isf32lem12  10366  isfin1-2  10387  hsmexlem4  10431  axcc2lem  10438  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  ac6num  10481  ac6s  10486  zorn2lem7  10504  ttukeylem5  10515  imadomg  10537  iundom2g  10548  ondomon  10571  ficard  10573  konigthlem  10577  alephreg  10591  pwcfsdom  10592  cfpwsdom  10593  axregndlem1  10611  axregnd  10613  pwfseqlem3  10669  pwxpndom2  10674  pwxpndom  10675  pwdjundom  10676  inawinalem  10698  gchina  10708  wuncval2  10756  tsk0  10772  tskxpss  10781  inatsk  10787  tskuni  10792  gruina  10827  grothac  10839  addclpi  10901  addnidpi  10910  nqereu  10938  mulcanenq  10969  genpnnp  11014  nqpr  11023  prlem934  11042  reclem2pr  11057  suplem1pr  11061  supsrlem  11120  axpre-sup  11178  1re  11232  dedekindle  11398  00id  11409  receu  11883  sup3  12196  infrelb  12224  peano5nni  12260  nnindd  12277  nnaddcl  12280  zrevaddcl  12663  nzadd  12666  zdiv  12691  nneo  12705  zeo2  12708  nn0indd  12718  fzind  12719  fnn0ind  12720  fzindd  12723  uzwo  12960  lbzbi  12985  nn01to3  12990  qrevaddcl  13021  irradd  13023  irrmul  13024  ltsubrp  13080  ltaddrp  13081  xnn0xaddcl  13287  xnn0xadd0  13299  icoshft  13526  fzen  13595  elfzm11  13650  uzsplit  13651  elfzom1elp1fzo  13788  fzoopth  13818  injresinjlem  13846  injresinj  13847  modifeq2int  13997  modsumfzodifsn  14008  om2uzlti  14014  ssnn0fi  14049  fsuppmapnn0fiub0  14057  mptnn0fsuppr  14063  seqcaopr3  14101  seqf1olem2a  14104  seqf1o  14107  ser1const  14122  expadd  14168  expmul  14171  leexp1a  14239  faccl  14347  facdiv  14351  faclbnd  14354  faclbnd4lem4  14360  hasheqf1oi  14415  hashgadd  14441  hashinfxadd  14449  hashunx  14450  hashunsng  14456  elprchashprn2  14460  hashss  14473  hash1snb  14484  hashmap  14500  hashf1lem2  14521  hashf1  14522  seqcoll  14529  hashle2pr  14542  hashdmpropge2  14548  hashge3el3dif  14552  hash1to3  14557  fundmge2nop0  14567  fi1uzind  14572  brfi1indALT  14575  sswrd  14587  swrdnd2  14725  swrdnnn0nd  14726  swrdnd0  14727  swrdwrdsymb  14732  pfxnd0  14758  swrdswrdlem  14773  swrdswrd  14774  wrd2ind  14792  swrdccatin1  14794  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccat3  14803  repsdf2  14849  repswswrd  14855  cshw0  14865  cshwcl  14869  cshwlen  14870  cshf1  14881  swrdco  14908  relexpsucnnl  15103  rtrclreclem3  15133  rtrclreclem4  15134  relexpindlem  15136  rtrclind  15138  shftlem  15141  sgn3da  15174  caubnd  15446  reusq0  15552  rlimcld2  15665  o1dif  15717  climub  15749  climserle  15750  iseraltlem2  15770  sumss  15810  fsumzcl2  15825  fsummsnunz  15840  fsumsplitsnun  15841  fsum2d  15857  modfsummods  15880  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  climcndslem1  15938  climcndslem2  15939  cvgrat  15972  clim2prod  15977  prodfn0  15983  prodfrec  15984  ntrivcvg  15986  prodmo  16023  fprodss  16035  fprodabs  16061  fprodn0  16066  fprod2d  16068  fprodefsum  16181  ruclem8  16325  ruclem9  16326  dvdsmod0  16348  dvds2ln  16379  dvdsaddre2b  16397  dvdslelem  16399  dvdsdivcl  16406  alzdvds  16410  mod2eq1n2dvds  16437  oddnn02np1  16438  nn0o1gt2  16471  nno  16472  sumeven  16477  sumodd  16478  pwp1fsum  16481  ndvdsadd  16500  bitsinv1  16532  sadcadd  16548  sadadd2  16550  saddisjlem  16554  smuval2  16572  smupvallem  16573  smu01lem  16575  smupval  16578  smueqlem  16580  smumullem  16582  gcddiv  16641  rplpwr  16648  nn0seqcvgd  16660  seq1st  16661  alginv  16665  algcvga  16669  algfx  16670  absprodnn  16708  isprm2  16772  isprm3  16773  prmind2  16775  maxprmfct  16800  prmdvdsexp  16806  pcmpt  16984  prmreclem4  17011  vdwmc2  17071  vdwlem10  17082  ramub2  17106  ramcl  17121  prmgaplem5  17147  prmgaplem8  17150  cshwshashlem1  17187  cshwshashlem3  17189  setsn0fun  17265  imasleval  17627  divsfval  17633  mreexexlem4d  17735  isssc  17909  initoeu1  18100  termoeu1  18107  istos  18504  chnfibg  18724  mgmcl  18733  sgrpidmnd  18841  frmdgsum  18971  smndex1mgm  19019  dfgrp3lem  19161  mhmmulg  19238  resghm2b  19361  gsumwrev  19493  elsymgbas  19501  symgextf1  19548  gsmsymgreqlem2  19558  gsmsymgreq  19559  odlem1  19662  odcl2  19692  gexlem1  19706  efgi2  19852  efginvrel2  19854  efgsrel  19861  cyggexb  20026  gsummulglem  20068  gsumzunsnd  20083  gsum2dlem2  20098  telgsums  20120  dmdprd  20127  dprdw  20139  ablfac1eulem  20201  srgpcomp  20357  rnghmmul  20590  nrhmzr  20699  lmodfopnelem1  21082  rmodislmodlem  21113  cnfldmulg  21617  cnfldexp  21618  nzerooringczr  21693  obslbs  21943  mplcoe1  22253  mplcoe3  22254  mplcoe5  22256  cply1mul  22521  coe1fzgsumdlem  22528  gsummoncoe1  22533  pf1ind  22580  evl1gsumdlem  22581  mat1dimcrng  22699  ma1repveval  22793  mulmarep1gsum2  22796  gsummatr01lem3  22879  matunitlindflem1  22901  cramerlem3  22914  decpmatmulsumfsupp  22998  mp2pm2mplem4  23034  pm2mpmhmlem1  23043  fvmptnn04if  23074  cayhamlem1  23091  fctop  23229  mretopd  23317  restopnb  23400  restdis  23403  tgcnp  23478  cncls2  23498  cncls  23499  cnntr  23500  cnsscnp  23504  cmpsub  23625  2ndcsep  23685  1stcelcls  23687  lfinpfin  23750  locfincmp  23752  comppfsc  23758  txcn  23852  txlm  23874  xkohaus  23879  qtopres  23924  haushmphlem  24013  cmphmph  24014  connhmph  24015  reghmph  24019  nrmhmph  24020  ptcmpfi  24039  reghaus  24051  fbssfi  24063  fbun  24066  fbfinnfr  24067  isfildlem  24083  fgcl  24104  cfinfil  24119  supfil  24121  ufinffr  24155  fin1aufil  24158  cnpflf  24227  alexsubALTlem3  24275  alexsubALT  24277  cnextfvval  24291  cnextcn  24293  tmdgsum  24321  tgphaus  24343  tgpt1  24344  mettri  24578  blssexps  24652  blssex  24653  mopni3  24720  metss  24734  psmetutop  24793  dscmet  24798  tngngp3  24882  rectbntr0  25059  metnrmlem1a  25085  fsumcn  25098  lmmbr  25486  caubl  25536  caublcls  25537  bcthlem5  25556  bcth3  25559  ovolunlem1a  25724  ovoliunnul  25735  finiunmbl  25772  voliunlem1  25778  volsuplem  25783  volsup  25784  dyadmax  25826  itgfsum  26054  dvnadd  26156  cpnord  26162  dvnfre  26179  dvmptfsum  26202  dvlip  26220  fta1g  26395  plyco  26467  dgrcolem1  26499  dgrco  26501  dvnply2  26517  plydivex  26527  plyexmo  26545  aannenlem1  26564  aaliou3lem2  26579  dvntaylp  26607  taylthlem1  26609  ulmval  26616  cxpmul2  26926  cxpsqrtth  26967  scvxcvx  27222  jensenlem2  27224  jensen  27225  ppiub  27440  bcmono  27513  bpos1lem  27518  bposlem5  27524  gausslemma2dlem6  27608  lgsquad2lem2  27621  2lgslem3  27640  2lgs  27643  2sqnn  27675  addsqnreup  27679  2sqreultblem  27684  2sqreunnltblem  27687  dchrisumlem1  27725  dchrisum0flb  27746  pntpbnd1  27822  pntlemf  27841  qabvle  27861  qabvexp  27862  ostthlem2  27864  ostth2lem2  27870  ltsval2  27892  ltssolem1  27911  negsprop  28300  mulsuniflem  28414  precsexlem6  28477  precsexlem7  28478  noseqind  28557  om2noseqlt  28564  n0addscl  28609  n0mulscl  28610  expsne0  28701  axeuclidlem  29419  axcontlem12  29432  umgrnloopv  29563  uhgredgrnv  29587  edglnl  29600  numedglnl  29601  usgruspgrb  29643  usgrnloopvALT  29661  usgredg2vlem2  29686  subupgr  29747  nbumgr  29807  uhgrnbgr0nb  29814  nbgr0edglem  29816  edgusgrnbfin  29833  nb3grprlem2  29841  uvtxnbgrvtx  29853  cplgrop  29897  cusgrfi  29918  fusgrmaxsize  29924  fusgrn0degnn0  29959  ewlkprop  30063  uspgr2wlkeq  30105  g0wlk0  30110  wlkreslem  30127  subgrwlk  30148  lfgriswlk  30150  upgrwlkdvde  30202  spthonepeq  30217  uhgrwkspth  30220  usgr2trlncl  30225  usgr2trlspth  30226  cyclnumvtx  30267  cyclnspth  30268  crctcshwlkn0lem3  30280  wwlksn  30305  wspthneq1eq2  30328  wwlksm1edg  30349  wwlksnred  30360  wwlksnextfun  30366  wwlksnextinj  30367  wwlksnextproplem3  30379  wspthsnonn0vne  30385  wspn0  30392  rusgrnumwwlk  30446  clwwlkccatlem  30459  umgrclwwlkge2  30461  clwlkclwwlklem2  30470  clwlkclwwlklem3  30471  clwwisshclwws  30485  clwwisshclwwsn  30486  clwwlkn1loopb  30513  wwlksext2clwwlk  30527  wwlksubclwwlk  30528  clwwlknonex2lem2  30578  upgr3v3e3cycl  30660  uhgr3cyclex  30662  upgr4cycl4dv4e  30665  eupth2lem3lem4  30711  eupth2lem3lem7  30714  eupth2  30719  eulerpath  30721  nfrgr2v  30752  frgr3vlem1  30753  3vfriswmgr  30758  1to2vfriswmgr  30759  1to3vfriswmgr  30760  3cyclfrgrrn1  30765  3cyclfrgrrn  30766  3cyclfrgrrn2  30767  4cycl2vnunb  30770  frgrncvvdeqlem2  30780  frgrncvvdeqlem8  30786  frgrncvvdeqlem9  30787  frgrwopreglem4a  30790  frgrwopreglem5lem  30800  frgrwopreglem5ALT  30802  frgrregorufr0  30804  frgr2wwlk1  30809  frgr2wwlkeqm  30811  fusgr2wsp2nb  30814  2wspmdisj  30817  frrusgrord  30821  numclwwlk1lem2f1  30837  numclwlk1  30851  frgrreggt1  30873  friendshipgt3  30878  hlim2  31673  elnlfn  32409  stle0i  32720  hstrbi  32747  spansncv2  32774  h1da  32830  fmptcof2  33130  xreceu  33367  domnprodn0  33718  1arithufdlem3  33956  1arithufdlem4  33957  tpr2rico  34422  hasheuni  34595  ismeas  34710  sseqp1  34906  rrvsum  34965  dstfrvunirn  34986  signstfvc  35082  bnj607  35425  bnj1145  35502  bnj1204  35521  r1filim  35612  fineqvrep  35640  fineqvnttrclselem1  35647  onvf1odlem4  35703  vonf1oonfo  35712  fisshasheq  35717  subfacp1lem6  35764  cvmlift2lem12  35893  cvmlift3lem4  35901  satfrnmapom  35949  sat1el2xp  35958  satffunlem2  35987  satffun  35988  mrsubvrs  36101  climuzcnv  36250  iprodefisumlem  36319  dfon2lem9  36368  linethru  36733  elhf2  36755  finminlem  36937  fnessref  36976  neibastop2lem  36979  fnemeet2  36986  nndivsub  37076  mh-inf3f1  37160  bj-cbvew  37372  bj-xpnzex  37703  bj-elpwg  37796  bj-epelg  37812  bj-axseprep  37819  mptsnunlem  38092  dissneqlem  38094  topdifinffinlem  38101  iooelexlt  38116  domalom  38158  fvineqsneq  38166  wl-exeq  38297  poimirlem22  38391  poimirlem26  38395  poimirlem28  38397  poimirlem29  38398  poimirlem32  38401  heicant  38404  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  cover2  38465  upixp  38479  sdclem2  38492  fdc  38495  seqpo  38497  metf1o  38505  mettrifi  38507  sstotbnd3  38526  heibor1lem  38559  heiborlem5  38565  heibor  38571  bfplem1  38572  elghomlem2OLD  38636  grpokerinj  38643  isrngo  38647  rngodm1dm2  38682  ispridl2  38788  exlimddvf  38869  lssatle  39888  4atexlemex4  40946  uzindd  42844  evl1gprodd  42983  sn-axprlem3  43088  redvmptabs  43235  sn-sup3d  43380  mzpsubst  43593  jm2.18  43829  wepwsolem  43883  oaabsb  44135  oacl2g  44171  ofoafg  44195  ofoaid1  44199  ofoaid2  44200  naddonnn  44236  iunrelexp0  44542  relexpmulg  44550  cnvtrclfv  44564  clsk1indlem3  44883  grucollcld  45084  inaex  45121  dvgrat  45136  radcnvrat  45138  csbxpgVD  45716  sineq0ALT  45759  trfr  45785  relwf  45790  pwclaxpow  45807  omssaxinf2  45811  islptre  46449  iblspltprt  46801  stoweidlem2  46830  stoweidlem17  46845  stoweidlem21  46849  2reuimp0  48002  2reuimp  48003  afveu  48041  funbrafv  48046  ndmaovass  48094  afv2eu  48126  tz6.12c-afv2  48130  funop1  48171  f1oresf1o2  48179  fvmptrabdm  48181  nltle2tri  48201  2elfz2melfz  48206  fsummsndifre  48268  fsumsplitsndif  48269  fsummmodsndifre  48270  fsummmodsnunz  48271  elsetpreimafvssdm  48286  uniimaelsetpreimafv  48296  imasetpreimafvbijlemfv1  48303  iccpartiltu  48322  iccpartigtl  48323  iccpartleu  48328  iccpartgel  48329  iccpartrn  48330  iccpartiun  48334  icceuelpart  48336  iccpartnel  48338  fargshiftf  48340  fargshiftf1  48341  ichnfb  48365  elsprel  48375  prsprel  48387  sprsymrelfo  48397  paireqne  48411  sbcpr  48421  reupr  48422  fmtnoinf  48439  odz2prm2pw  48466  lighneallem4  48513  lighneal  48514  requad1  48538  requad2  48539  evensumeven  48623  even3prm2  48635  gbowgt5  48678  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbnnsum3prm  48720  bgoldbtbndlem2  48722  bgoldbtbndlem4  48724  bgoldbtbnd  48725  dfsclnbgr6  48774  grimco  48805  cycl3grtri  48863  isubgr3stgrlem6  48887  gricgrlic  48934  gpgedgvtx0  48977  gpgprismgr4cycllem3  49013  pgnbgreunbgrlem5  49039  clcllaw  49106  rngccatidALTV  49187  ringccatidALTV  49221  scmsuppss  49301  gsumlsscl  49310  ply1mulgsumlem2  49317  lincvalsc0  49351  linc0scn0  49353  lincdifsn  49354  linc1  49355  lincellss  49356  lincsum  49359  lincscm  49360  lincsumcl  49361  lcoss  49366  lincext3  49386  lindslinindimp2lem4  49391  lindslinindsimp2lem5  49392  lindslinindsimp2  49393  lindsrng01  49398  snlindsntor  49401  lincresunit3lem2  49410  lincresunit3  49411  islindeps2  49413  blengt1fldiv2p1  49523  2arymaptf1  49583  resum2sqorgt0  49639  reorelicc  49640  rrx2plordisom  49653  rrx2linest  49672  rrxsphere  49678  line2ylem  49681  itsclc0xyqsol  49698  itscnhlinecirc02p  49715  mo0sn  49744  thincn0eu  50357  alsralrex  50741  alsraln0  50742