Theorem expcom 418

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ancoms  463  pm3.21  476  sylan  591  animpimp2impd  859  4casesdan  1057  dedlema  1061  dedlemb  1062  sbiedvw  2130  mo4  2594  2moswapv  2657  2moswap  2672  2eu2  2680  pm2.61ne  3043  nelelne  3059  r19.21be  3258  rspcebdv  3576  2reu2  3853  csbie2df  4409  minel  4427  uneqdifeq  4454  raltpd  4748  ssunsn2  4794  opthprneg  4831  ssuni  4899  uniss2  4908  elpwuni  5072  intss2  5075  disjord  5099  elpw2g  5305  elssabg  5315  axprlem3OLD  5402  axprlem4OLD  5403  axprlem5OLD  5404  axprglem  5409  oteqex  5485  otsndisj  5504  otiunsndisj  5505  epelg  5564  wereu  5659  relop  5838  riinint  5964  sotri3  6132  unixpid  6287  reuop  6296  ordtr2  6408  ordsssuc2  6456  iotan0  6528  funopg  6572  fun  6742  fvmptnf  7014  fvn0ssdmfun  7071  eldmrexrnb  7089  fmptco  7127  fnressn  7157  fressnfv  7159  fprb  7194  fvtp2g  7199  fvtp3g  7200  fconst2g  7203  fntpb  7209  f1dom3el3dif  7269  f1ounsn  7272  isores3  7335  isoselem  7341  oprabv  7472  eloprabga  7521  sorpsscmpl  7733  difex2  7760  ordpwsuc  7812  ordsucun  7822  limuni3  7849  trom  7872  fo1stres  8013  poxp  8125  soxp  8126  xpord3inddlem  8151  soseq  8156  suppimacnv  8171  fsuppeq  8172  funsssuppss  8187  brtpos2  8229  frrlem8  8291  fpr2a  8300  onnseq  8332  smores  8340  smofvon2  8344  tfrlem1  8363  oacl  8521  omcl  8522  oecl  8523  oawordri  8536  oalimcl  8546  oaass  8547  oarec  8548  omwordri  8558  omeulem1  8568  omeulem2  8569  oeordi  8574  oeworde  8580  oeoelem  8585  nnacl  8598  nnmcl  8599  nnecl  8600  nnacom  8604  nnaass  8609  nnmsucr  8612  nnmordi  8618  omabs  8638  cofonr  8661  naddunif  8681  iiner  8788  elpmg  8841  fsetfcdm  8858  fsetprcnex  8860  pmss12g  8868  mapfvd  8878  f1domg  8969  ssdomg  8998  undom  9054  domtriord  9112  ssnnfi  9155  fnfi  9163  enfi  9172  php  9192  sdom1  9211  1sdom2dom  9215  fisseneq  9224  isinf  9226  dif1ennnALT  9238  findcard3  9244  frfi  9246  difinf  9272  iunfi  9301  fsuppunfi  9349  fsuppres  9354  ffsuppbi  9359  elfi2  9375  marypha1lem  9394  marypha1  9395  oiexg  9498  wemapso2  9516  harword  9526  brwdom  9530  unxpwdom  9552  en3lplem1  9582  inf3lemd  9597  inf3lem5  9602  cantnfval2  9639  cantnfle  9641  cantnflt  9642  cnfcom  9670  tcmin  9709  frr2  9733  r1sdom  9747  rankxplim3  9854  cardidm  9946  cardmin2  9986  infxpenlem  9998  fseqenlem1  10009  numacn  10034  alephordi  10059  iscard3  10078  alephinit  10080  carduniima  10081  iunfictbso  10099  dfac5  10113  dfac12lem3  10130  nnadju  10182  pwsdompw  10187  pwdjudom  10199  cflim2  10248  cfslb2n  10253  cofsmo  10254  cfsmolem  10255  cfcoflem  10257  alephsing  10261  infpssALT  10298  fin23lem34  10331  isf32lem2  10339  isf32lem10  10347  isf32lem12  10349  isfin1-2  10370  hsmexlem4  10414  axcc2lem  10421  domtriomlem  10427  axdc2lem  10433  axdc3lem2  10436  axdc3lem4  10438  axdc4lem  10440  axcclem  10442  ac6num  10464  ac6s  10469  zorn2lem7  10487  ttukeylem5  10498  imadomg  10519  iundom2g  10525  ondomon  10548  ficard  10550  konigthlem  10554  alephreg  10568  pwcfsdom  10569  cfpwsdom  10570  axregndlem1  10588  axregnd  10590  pwfseqlem3  10646  pwxpndom2  10651  pwxpndom  10652  pwdjundom  10653  inawinalem  10675  gchina  10685  wuncval2  10733  tsk0  10749  tskxpss  10758  inatsk  10764  tskuni  10769  gruina  10804  grothac  10816  addclpi  10878  addnidpi  10887  nqereu  10915  mulcanenq  10946  genpnnp  10991  nqpr  11000  prlem934  11019  reclem2pr  11034  suplem1pr  11038  supsrlem  11097  axpre-sup  11155  1re  11209  dedekindle  11375  00id  11386  receu  11860  sup3  12173  infrelb  12201  peano5nni  12237  nnindd  12254  nnaddcl  12257  zrevaddcl  12640  nzadd  12643  zdiv  12667  nneo  12681  zeo2  12684  nn0indd  12694  fzind  12695  fnn0ind  12696  fzindd  12699  uzwo  12936  lbzbi  12961  nn01to3  12966  qrevaddcl  12996  irradd  12998  irrmul  12999  ltsubrp  13055  ltaddrp  13056  xnn0xaddcl  13262  xnn0xadd0  13274  icoshft  13501  fzen  13570  elfzm11  13625  uzsplit  13626  elfzom1elp1fzo  13763  fzoopth  13793  injresinjlem  13821  injresinj  13822  modifeq2int  13971  modsumfzodifsn  13982  om2uzlti  13988  ssnn0fi  14023  fsuppmapnn0fiub0  14031  mptnn0fsuppr  14037  seqcaopr3  14075  seqf1olem2a  14078  seqf1o  14081  ser1const  14096  expadd  14142  expmul  14145  leexp1a  14213  faccl  14321  facdiv  14325  faclbnd  14328  faclbnd4lem4  14334  hasheqf1oi  14389  hashgadd  14415  hashinfxadd  14423  hashunx  14424  hashunsng  14430  elprchashprn2  14434  hashss  14447  hash1snb  14458  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  hashle2pr  14516  hashdmpropge2  14522  hashge3el3dif  14526  hash1to3  14531  fundmge2nop0  14541  fi1uzind  14546  brfi1indALT  14549  sswrd  14561  swrdnd2  14695  swrdnnn0nd  14696  swrdnd0  14697  swrdwrdsymb  14702  pfxnd0  14728  swrdswrdlem  14743  swrdswrd  14744  wrd2ind  14762  swrdccatin1  14764  swrdccatin2  14768  pfxccatin12lem2  14770  pfxccat3  14773  repsdf2  14817  repswswrd  14823  cshw0  14833  cshwcl  14837  cshwlen  14838  cshf1  14849  swrdco  14876  relexpsucnnl  15069  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  shftlem  15107  sgn3da  15140  caubnd  15412  reusq0  15518  rlimcld2  15631  o1dif  15683  climub  15715  climserle  15716  iseraltlem2  15736  sumss  15777  fsumzcl2  15792  fsummsnunz  15807  fsumsplitsnun  15808  fsum2d  15824  modfsummods  15847  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  climcndslem1  15905  climcndslem2  15906  cvgrat  15939  clim2prod  15944  prodfn0  15950  prodfrec  15951  ntrivcvg  15953  prodmo  15992  fprodss  16004  fprodabs  16030  fprodn0  16035  fprod2d  16037  fprodefsum  16150  ruclem8  16294  ruclem9  16295  dvdsmod0  16317  dvds2ln  16348  dvdsaddre2b  16366  dvdslelem  16368  dvdsdivcl  16375  alzdvds  16379  mod2eq1n2dvds  16406  oddnn02np1  16407  nn0o1gt2  16440  nno  16441  sumeven  16446  sumodd  16447  pwp1fsum  16450  ndvdsadd  16469  bitsinv1  16501  sadcadd  16517  sadadd2  16519  saddisjlem  16523  smuval2  16541  smupvallem  16542  smu01lem  16544  smupval  16547  smueqlem  16549  smumullem  16551  gcddiv  16610  rplpwr  16617  nn0seqcvgd  16629  seq1st  16630  alginv  16634  algcvga  16638  algfx  16639  absprodnn  16677  isprm2  16741  isprm3  16742  prmind2  16744  maxprmfct  16769  prmdvdsexp  16775  pcmpt  16953  prmreclem4  16980  vdwmc2  17040  vdwlem10  17051  ramub2  17075  ramcl  17090  prmgaplem5  17116  prmgaplem8  17119  cshwshashlem1  17156  cshwshashlem3  17158  setsn0fun  17234  imasleval  17596  divsfval  17602  mreexexlem4d  17704  isssc  17878  initoeu1  18069  termoeu1  18076  istos  18473  chnfibg  18693  mgmcl  18702  sgrpidmnd  18798  frmdgsum  18922  smndex1mgm  18970  dfgrp3lem  19105  mhmmulg  19182  resghm2b  19305  gsumwrev  19437  elsymgbas  19445  symgextf1  19492  gsmsymgreqlem2  19502  gsmsymgreq  19503  odlem1  19606  odcl2  19636  gexlem1  19650  efgi2  19796  efginvrel2  19798  efgsrel  19805  cyggexb  19970  gsummulglem  20012  gsumzunsnd  20027  gsum2dlem2  20042  telgsums  20064  dmdprd  20071  dprdw  20083  ablfac1eulem  20145  srgpcomp  20301  rnghmmul  20532  nrhmzr  20623  lmodfopnelem1  21000  rmodislmodlem  21031  cnfldmulg  21535  cnfldexp  21536  nzerooringczr  21611  obslbs  21861  mplcoe1  22169  mplcoe3  22170  mplcoe5  22172  cply1mul  22437  coe1fzgsumdlem  22444  gsummoncoe1  22449  pf1ind  22496  evl1gsumdlem  22497  mat1dimcrng  22615  ma1repveval  22709  mulmarep1gsum2  22712  gsummatr01lem3  22795  cramerlem3  22827  decpmatmulsumfsupp  22911  mp2pm2mplem4  22947  pm2mpmhmlem1  22956  fvmptnn04if  22987  cayhamlem1  23004  fctop  23142  mretopd  23230  restopnb  23313  restdis  23316  tgcnp  23391  cncls2  23411  cncls  23412  cnntr  23413  cnsscnp  23417  cmpsub  23538  2ndcsep  23597  1stcelcls  23599  lfinpfin  23662  locfincmp  23664  comppfsc  23670  txcn  23764  txlm  23786  xkohaus  23791  qtopres  23836  haushmphlem  23925  cmphmph  23926  connhmph  23927  reghmph  23931  nrmhmph  23932  ptcmpfi  23951  reghaus  23963  fbssfi  23975  fbun  23978  fbfinnfr  23979  isfildlem  23995  fgcl  24016  cfinfil  24031  supfil  24033  ufinffr  24067  fin1aufil  24070  cnpflf  24139  alexsubALTlem3  24187  alexsubALT  24189  cnextfvval  24203  cnextcn  24205  tmdgsum  24233  tgphaus  24255  tgpt1  24256  mettri  24490  blssexps  24564  blssex  24565  mopni3  24632  metss  24646  psmetutop  24705  dscmet  24710  tngngp3  24794  rectbntr0  24971  metnrmlem1a  24997  fsumcn  25010  lmmbr  25398  caubl  25448  caublcls  25449  bcthlem5  25468  bcth3  25471  ovolunlem1a  25636  ovoliunnul  25647  finiunmbl  25684  voliunlem1  25690  volsuplem  25695  volsup  25696  dyadmax  25738  itgfsum  25967  dvnadd  26069  cpnord  26075  dvnfre  26092  dvmptfsum  26115  dvlip  26133  fta1g  26308  plyco  26379  dgrcolem1  26411  dgrco  26413  dvnply2  26429  plydivex  26439  plyexmo  26455  aannenlem1  26472  aaliou3lem2  26487  dvntaylp  26515  taylthlem1  26517  ulmval  26524  cxpmul2  26835  cxpsqrtth  26876  scvxcvx  27131  jensenlem2  27133  jensen  27134  ppiub  27349  bcmono  27422  bpos1lem  27427  bposlem5  27433  gausslemma2dlem6  27517  lgsquad2lem2  27530  2lgslem3  27549  2lgs  27552  2sqnn  27584  addsqnreup  27588  2sqreultblem  27593  2sqreunnltblem  27596  dchrisumlem1  27634  dchrisum0flb  27655  pntpbnd1  27731  pntlemf  27750  qabvle  27770  qabvexp  27771  ostthlem2  27773  ostth2lem2  27779  ltsval2  27801  ltssolem1  27820  negsprop  28209  mulsuniflem  28323  precsexlem6  28386  precsexlem7  28387  noseqind  28466  om2noseqlt  28473  n0addscl  28518  n0mulscl  28519  expsne0  28610  axeuclidlem  29293  axcontlem12  29306  umgrnloopv  29437  uhgredgrnv  29461  edglnl  29474  numedglnl  29475  usgruspgrb  29514  usgrnloopvALT  29532  usgredg2vlem2  29557  subupgr  29618  nbumgr  29678  uhgrnbgr0nb  29685  nbgr0edglem  29687  edgusgrnbfin  29704  nb3grprlem2  29712  uvtxnbgrvtx  29724  cplgrop  29768  cusgrfi  29789  fusgrmaxsize  29795  fusgrn0degnn0  29830  ewlkprop  29934  uspgr2wlkeq  29976  g0wlk0  29981  wlkreslem  29998  lfgriswlk  30017  upgrwlkdvde  30067  spthonepeq  30082  uhgrwkspth  30085  usgr2trlncl  30090  usgr2trlspth  30091  cyclnumvtx  30130  cyclnspth  30131  crctcshwlkn0lem3  30142  wwlksn  30167  wspthneq1eq2  30190  wwlksm1edg  30211  wwlksnred  30222  wwlksnextfun  30228  wwlksnextinj  30229  wwlksnextproplem3  30241  wspthsnonn0vne  30247  wspn0  30254  rusgrnumwwlk  30308  clwwlkccatlem  30321  umgrclwwlkge2  30323  clwlkclwwlklem2  30332  clwlkclwwlklem3  30333  clwwisshclwws  30347  clwwisshclwwsn  30348  clwwlkn1loopb  30375  wwlksext2clwwlk  30389  wwlksubclwwlk  30390  clwwlknonex2lem2  30440  upgr3v3e3cycl  30512  uhgr3cyclex  30514  upgr4cycl4dv4e  30517  eupth2lem3lem4  30563  eupth2lem3lem7  30566  eupth2  30571  eulerpath  30573  nfrgr2v  30604  frgr3vlem1  30605  3vfriswmgr  30610  1to2vfriswmgr  30611  1to3vfriswmgr  30612  3cyclfrgrrn1  30617  3cyclfrgrrn  30618  3cyclfrgrrn2  30619  4cycl2vnunb  30622  frgrncvvdeqlem2  30632  frgrncvvdeqlem8  30638  frgrncvvdeqlem9  30639  frgrwopreglem4a  30642  frgrwopreglem5lem  30652  frgrwopreglem5ALT  30654  frgrregorufr0  30656  frgr2wwlk1  30661  frgr2wwlkeqm  30663  fusgr2wsp2nb  30666  2wspmdisj  30669  frrusgrord  30673  numclwwlk1lem2f1  30689  numclwlk1  30703  frgrreggt1  30725  friendshipgt3  30730  hlim2  31525  elnlfn  32261  stle0i  32572  hstrbi  32599  spansncv2  32626  h1da  32682  fmptcof2  32983  xreceu  33222  domnprodn0  33579  1arithufdlem3  33817  1arithufdlem4  33818  tpr2rico  34283  hasheuni  34456  ismeas  34570  sseqp1  34766  rrvsum  34825  dstfrvunirn  34846  signstfvc  34942  bnj607  35285  bnj1145  35362  bnj1204  35381  r1filim  35479  fineqvrep  35508  fineqvnttrclselem1  35515  onvf1odlem4  35571  vonf1oonfo  35580  fisshasheq  35587  subgrwlk  35605  subfacp1lem6  35658  cvmlift2lem12  35787  cvmlift3lem4  35795  satfrnmapom  35843  sat1el2xp  35852  satffunlem2  35881  satffun  35882  mrsubvrs  35995  climuzcnv  36144  iprodefisumlem  36213  dfon2lem9  36262  linethru  36626  elhf2  36648  finminlem  36810  fnessref  36849  neibastop2lem  36852  fnemeet2  36859  nndivsub  36949  mh-inf3f1  37033  bj-cbvew  37245  bj-xpnzex  37576  bj-elpwg  37669  bj-epelg  37685  bj-axseprep  37692  mptsnunlem  37965  dissneqlem  37967  topdifinffinlem  37974  iooelexlt  37989  domalom  38031  fvineqsneq  38039  wl-exeq  38170  matunitlindflem1  38248  poimirlem22  38274  poimirlem26  38278  poimirlem28  38280  poimirlem29  38281  poimirlem32  38284  heicant  38287  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  cover2  38347  upixp  38361  sdclem2  38374  fdc  38377  seqpo  38379  metf1o  38387  mettrifi  38389  sstotbnd3  38408  heibor1lem  38441  heiborlem5  38447  heibor  38453  bfplem1  38454  elghomlem2OLD  38518  grpokerinj  38525  isrngo  38529  rngodm1dm2  38564  ispridl2  38670  exlimddvf  38751  lssatle  39770  4atexlemex4  40828  uzindd  42726  evl1gprodd  42865  sn-axprlem3  42970  redvmptabs  43102  sn-sup3d  43247  mzpsubst  43462  jm2.18  43698  wepwsolem  43752  oaabsb  44004  oacl2g  44040  ofoafg  44064  ofoaid1  44068  ofoaid2  44069  naddonnn  44105  iunrelexp0  44411  relexpmulg  44419  cnvtrclfv  44433  clsk1indlem3  44752  grucollcld  44953  inaex  44990  dvgrat  45005  radcnvrat  45007  csbxpgVD  45585  sineq0ALT  45628  trfr  45654  relwf  45659  pwclaxpow  45676  omssaxinf2  45680  islptre  46318  iblspltprt  46670  stoweidlem2  46699  stoweidlem17  46714  stoweidlem21  46718  2reuimp0  47834  2reuimp  47835  afveu  47873  funbrafv  47878  ndmaovass  47926  afv2eu  47958  tz6.12c-afv2  47962  funop1  48003  f1oresf1o2  48011  fvmptrabdm  48013  nltle2tri  48033  2elfz2melfz  48038  fsummsndifre  48100  fsumsplitsndif  48101  fsummmodsndifre  48102  fsummmodsnunz  48103  elsetpreimafvssdm  48118  uniimaelsetpreimafv  48128  imasetpreimafvbijlemfv1  48135  iccpartiltu  48154  iccpartigtl  48155  iccpartleu  48160  iccpartgel  48161  iccpartrn  48162  iccpartiun  48166  icceuelpart  48168  iccpartnel  48170  fargshiftf  48172  fargshiftf1  48173  ichnfb  48197  elsprel  48207  prsprel  48219  sprsymrelfo  48229  paireqne  48243  sbcpr  48253  reupr  48254  fmtnoinf  48271  odz2prm2pw  48298  lighneallem4  48345  lighneal  48346  requad1  48370  requad2  48371  evensumeven  48455  even3prm2  48467  gbowgt5  48510  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  bgoldbnnsum3prm  48552  bgoldbtbndlem2  48554  bgoldbtbndlem4  48556  bgoldbtbnd  48557  dfsclnbgr6  48606  grimco  48637  cycl3grtri  48695  isubgr3stgrlem6  48719  gricgrlic  48766  gpgedgvtx0  48809  gpgprismgr4cycllem3  48845  pgnbgreunbgrlem5  48871  clcllaw  48939  rngccatidALTV  49020  ringccatidALTV  49054  scmsuppss  49134  gsumlsscl  49143  ply1mulgsumlem2  49150  lincvalsc0  49184  linc0scn0  49186  lincdifsn  49187  linc1  49188  lincellss  49189  lincsum  49192  lincscm  49193  lincsumcl  49194  lcoss  49199  lincext3  49219  lindslinindimp2lem4  49224  lindslinindsimp2lem5  49225  lindslinindsimp2  49226  lindsrng01  49231  snlindsntor  49234  lincresunit3lem2  49243  lincresunit3  49244  islindeps2  49246  blengt1fldiv2p1  49356  2arymaptf1  49416  resum2sqorgt0  49472  reorelicc  49473  rrx2plordisom  49486  rrx2linest  49505  rrxsphere  49511  line2ylem  49514  itsclc0xyqsol  49531  itscnhlinecirc02p  49548  mo0sn  49577  thincn0eu  50192  alsralrex  50573  alsraln0  50574