Theorem expcom 416

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ancoms  461  pm3.21  474  sylan  582  animpimp2impd  842  4casesdan  1036  dedlema  1040  dedlemb  1041  sbiedvw  2104  cbval2vOLD  2364  cbval2OLD  2433  mo4  2650  2moswapv  2714  2moswap  2729  2mos  2734  2eu2  2737  pm2.61ne  3102  nelelne  3117  r19.21be  3210  cbvraldva2  3456  cbvrexdva2OLD  3458  rspcebdv  3617  2reu2  3882  csbie2df  4392  minel  4415  uneqdifeq  4438  raltpd  4716  ssunsn2  4760  opthprneg  4795  ssuni  4863  uniss2  4871  elpwuni  5027  disjord  5054  elssabg  5239  elpw2g  5247  axprlem3  5326  axprlem4  5327  axprlem5  5328  oteqex  5390  otsndisj  5409  otiunsndisj  5410  epelg  5466  epelgOLD  5467  wereu  5551  relop  5721  riinint  5839  sotri3  5990  unixpid  6135  reuop  6144  ordtr2  6235  ordsssuc2  6279  iotan0  6345  funopg  6389  fun  6540  tz6.12c  6695  fvmptnf  6790  fvn0ssdmfun  6842  eldmrexrnb  6858  fmptco  6891  fnressn  6920  fressnfv  6922  fprb  6956  fvtp2g  6961  fvtp3g  6962  fconst2g  6965  fntpb  6972  f1dom3el3dif  7027  isores3  7088  isoselem  7094  oprabv  7214  eloprabga  7261  sorpsscmpl  7460  difex2  7482  ordpwsuc  7530  ordsucun  7540  limuni3  7567  ordom  7589  fo1stres  7715  poxp  7822  soxp  7823  suppimacnv  7841  frnsuppeq  7842  funsssuppss  7856  brtpos2  7898  wfrlem12  7966  onnseq  7981  smores  7989  smofvon2  7993  tfrlem1  8012  oacl  8160  omcl  8161  oecl  8162  oawordri  8176  oalimcl  8186  oaass  8187  oarec  8188  omwordri  8198  omeulem1  8208  omeulem2  8209  oeordi  8213  oeworde  8219  oeoelem  8224  nnacl  8237  nnmcl  8238  nnecl  8239  nnacom  8243  nnaass  8248  nnmsucr  8251  nnmordi  8257  omabs  8274  iiner  8369  elpmg  8422  pmss12g  8433  mapfvd  8443  f1domg  8529  ssdomg  8555  domtriord  8663  php  8701  php3  8703  1sdom  8721  fisseneq  8729  isinf  8731  ssnnfi  8737  dif1en  8751  findcard3  8761  frfi  8763  unfi  8785  difinf  8788  fnfi  8796  iunfi  8812  fsuppunfi  8853  fsuppres  8858  frnfsuppbi  8862  elfi2  8878  marypha1lem  8897  marypha1  8898  oiexg  8999  wemapso2  9017  harword  9029  brwdom  9031  unxpwdom  9053  en3lplem1  9075  inf3lemd  9090  inf3lem5  9095  cantnfval2  9132  cantnfle  9134  cantnflt  9135  cnfcom  9163  tcmin  9183  r1sdom  9203  rankxplim3  9310  cardidm  9388  cardmin2  9427  infxpenlem  9439  fseqenlem1  9450  numacn  9475  alephordi  9500  iscard3  9519  alephinit  9521  carduniima  9522  iunfictbso  9540  dfac5  9554  dfac12lem3  9571  pwsdompw  9626  pwdjudom  9638  cflim2  9685  cfslb2n  9690  cofsmo  9691  cfsmolem  9692  cfcoflem  9694  alephsing  9698  infpssALT  9735  fin23lem34  9768  isf32lem2  9776  isf32lem10  9784  isf32lem12  9786  isfin1-2  9807  hsmexlem4  9851  axcc2lem  9858  domtriomlem  9864  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  ac6num  9901  ac6s  9906  zorn2lem7  9924  ttukeylem5  9935  imadomg  9956  iundom2g  9962  ondomon  9985  ficard  9987  konigthlem  9990  alephreg  10004  pwcfsdom  10005  cfpwsdom  10006  axregndlem1  10024  axregnd  10026  pwfseqlem3  10082  pwxpndom2  10087  pwxpndom  10088  pwdjundom  10089  inawinalem  10111  gchina  10121  wuncval2  10169  tsk0  10185  tskxpss  10194  inatsk  10200  tskuni  10205  gruina  10240  grothac  10252  addclpi  10314  addnidpi  10323  nqereu  10351  mulcanenq  10382  genpnnp  10427  nqpr  10436  prlem934  10455  reclem2pr  10470  suplem1pr  10474  supsrlem  10533  axpre-sup  10591  1re  10641  dedekindle  10804  00id  10815  receu  11285  sup3  11598  infrelb  11626  peano5nni  11641  nnindd  11658  nnaddcl  11661  zrevaddcl  12028  nzadd  12031  zdiv  12053  nneo  12067  zeo2  12070  nn0indd  12080  fzind  12081  fnn0ind  12082  uzwo  12312  lbzbi  12337  nn01to3  12342  qrevaddcl  12371  irradd  12373  irrmul  12374  ltsubrp  12426  ltaddrp  12427  xnn0xaddcl  12629  xnn0xadd0  12641  icoshft  12860  fzen  12925  elfzm11  12979  uzsplit  12980  elfzoext  13095  elfzom1elp1fzo  13105  injresinjlem  13158  injresinj  13159  modifeq2int  13302  modsumfzodifsn  13313  om2uzlti  13319  ssnn0fi  13354  fsuppmapnn0fiub0  13362  mptnn0fsuppr  13368  seqcaopr3  13406  seqf1olem2a  13409  seqf1o  13412  ser1const  13427  expadd  13472  expmul  13475  leexp1a  13540  faccl  13644  facdiv  13648  faclbnd  13651  faclbnd4lem4  13657  hasheqf1oi  13713  hashgadd  13739  hashinfxadd  13747  hashunx  13748  hashunsng  13754  elprchashprn2  13758  hashss  13771  hash1snb  13781  hashmap  13797  hashf1lem2  13815  hashf1  13816  seqcoll  13823  hashle2pr  13836  hashdmpropge2  13842  hashge3el3dif  13845  hash1to3  13850  fundmge2nop0  13851  fi1uzind  13856  brfi1indALT  13859  sswrd  13870  swrdnd2  14017  swrdnnn0nd  14018  swrdnd0  14019  swrdwrdsymb  14024  pfxnd0  14050  swrdswrdlem  14066  swrdswrd  14067  wrd2ind  14085  swrdccatin1  14087  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccat3  14096  repsdf2  14140  repswswrd  14146  cshw0  14156  cshwcl  14160  cshwlen  14161  cshf1  14172  swrdco  14199  relexpsucnnl  14391  rtrclreclem3  14419  rtrclreclem4  14420  relexpindlem  14422  rtrclind  14424  shftlem  14427  caubnd  14718  reusq0  14822  rlimcld2  14935  o1dif  14986  climub  15018  climserle  15019  iseraltlem2  15039  sumss  15081  fsumzcl2  15095  fsummsnunz  15109  fsumsplitsnun  15110  fsum2d  15126  modfsummods  15148  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  climcndslem1  15204  climcndslem2  15205  cvgrat  15239  clim2prod  15244  prodfn0  15250  prodfrec  15251  ntrivcvg  15253  prodmo  15290  fprodss  15302  fprodabs  15328  fprodn0  15333  fprod2d  15335  fprodefsum  15448  ruclem8  15590  ruclem9  15591  dvdsmod0  15613  dvds2ln  15642  dvdsaddre2b  15657  dvdslelem  15659  dvdsdivcl  15666  alzdvds  15670  mod2eq1n2dvds  15696  oddnn02np1  15697  nn0o1gt2  15732  nno  15733  sumeven  15738  sumodd  15739  pwp1fsum  15742  ndvdsadd  15761  bitsinv1  15791  sadcadd  15807  sadadd2  15809  saddisjlem  15813  smuval2  15831  smupvallem  15832  smu01lem  15834  smupval  15837  smueqlem  15839  smumullem  15841  gcddiv  15899  gcdmultipleOLD  15900  rplpwr  15907  nn0seqcvgd  15914  seq1st  15915  alginv  15919  algcvga  15923  algfx  15924  absprodnn  15962  isprm2  16026  isprm3  16027  prmind2  16029  maxprmfct  16053  prmdvdsexp  16059  pcmpt  16228  prmreclem4  16255  vdwmc2  16315  vdwlem10  16326  ramub2  16350  ramcl  16365  prmgaplem5  16391  prmgaplem8  16394  cshwshashlem1  16429  cshwshashlem3  16431  setsn0fun  16520  imasleval  16814  divsfval  16820  mreexexlem4d  16918  isssc  17090  initoeu1  17271  termoeu1  17278  istos  17645  mgmcl  17855  sgrpidmnd  17916  frmdgsum  18027  smndex1mgm  18072  dfgrp3lem  18197  mhmmulg  18268  resghm2b  18376  gsumwrev  18494  elsymgbas  18502  symgextf1  18549  gsmsymgreqlem2  18559  gsmsymgreq  18560  odlem1  18663  odcl2  18692  gexlem1  18704  efgi2  18851  efginvrel2  18853  efgsrel  18860  cyggexb  19019  gsummulglem  19061  gsumzunsnd  19076  gsum2dlem2  19091  telgsums  19113  dmdprd  19120  dprdw  19132  ablfac1eulem  19194  srgpcomp  19282  lmodfopnelem1  19670  rmodislmodlem  19701  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  cply1mul  20462  coe1fzgsumdlem  20469  gsummoncoe1  20472  pf1ind  20518  evl1gsumdlem  20519  cnfldmulg  20577  cnfldexp  20578  obslbs  20874  mat1dimcrng  21086  ma1repveval  21180  mulmarep1gsum2  21183  gsummatr01lem3  21266  cramerlem3  21298  decpmatmulsumfsupp  21381  mp2pm2mplem4  21417  pm2mpmhmlem1  21426  fvmptnn04if  21457  cayhamlem1  21474  fctop  21612  mretopd  21700  restopnb  21783  restdis  21786  tgcnp  21861  cncls2  21881  cncls  21882  cnntr  21883  cnsscnp  21887  cmpsub  22008  2ndcsep  22067  1stcelcls  22069  lfinpfin  22132  locfincmp  22134  comppfsc  22140  txcn  22234  txlm  22256  xkohaus  22261  qtopres  22306  haushmphlem  22395  cmphmph  22396  connhmph  22397  reghmph  22401  nrmhmph  22402  ptcmpfi  22421  reghaus  22433  fbssfi  22445  fbun  22448  fbfinnfr  22449  isfildlem  22465  fgcl  22486  cfinfil  22501  supfil  22503  ufinffr  22537  fin1aufil  22540  cnpflf  22609  alexsubALTlem3  22657  alexsubALT  22659  cnextfvval  22673  cnextcn  22675  tmdgsum  22703  tgphaus  22725  tgpt1  22726  mettri  22962  blssexps  23036  blssex  23037  mopni3  23104  metss  23118  psmetutop  23177  dscmet  23182  tngngp3  23265  rectbntr0  23440  metnrmlem1a  23466  fsumcn  23478  lmmbr  23861  caubl  23911  caublcls  23912  bcthlem5  23931  bcth3  23934  ovolunlem1a  24097  ovoliunnul  24108  finiunmbl  24145  voliunlem1  24151  volsuplem  24156  volsup  24157  dyadmax  24199  itgfsum  24427  dvnadd  24526  cpnord  24532  dvnfre  24549  dvmptfsum  24572  dvlip  24590  fta1g  24761  plyco  24831  dgrcolem1  24863  dgrco  24865  dvnply2  24876  plydivex  24886  plyexmo  24902  aannenlem1  24917  aaliou3lem2  24932  dvntaylp  24959  taylthlem1  24961  ulmval  24968  cxpmul2  25272  cxpsqrtth  25312  scvxcvx  25563  jensenlem2  25565  jensen  25566  ppiub  25780  bcmono  25853  bpos1lem  25858  bposlem5  25864  gausslemma2dlem6  25948  lgsquad2lem2  25961  2lgslem3  25980  2lgs  25983  2sqnn  26015  addsqnreup  26019  2sqreultblem  26024  2sqreunnltblem  26027  dchrisumlem1  26065  dchrisum0flb  26086  pntpbnd1  26162  pntlemf  26181  qabvle  26201  qabvexp  26202  ostthlem2  26204  ostth2lem2  26210  axeuclidlem  26748  axcontlem12  26761  umgrnloopv  26891  uhgredgrnv  26915  edglnl  26928  numedglnl  26929  usgruspgrb  26966  usgrnloopvALT  26983  usgredg2vlem2  27008  subupgr  27069  nbumgr  27129  uhgrnbgr0nb  27136  nbgr0vtxlem  27137  edgusgrnbfin  27155  nb3grprlem2  27163  uvtxnbgrvtx  27175  cplgrop  27219  cusgrfi  27240  fusgrmaxsize  27246  fusgrn0degnn0  27281  ewlkprop  27385  uspgr2wlkeq  27427  g0wlk0  27433  wlkreslem  27451  lfgriswlk  27470  upgrwlkdvde  27518  spthonepeq  27533  uhgrwkspth  27536  usgr2trlncl  27541  usgr2trlspth  27542  cyclnspth  27581  crctcshwlkn0lem3  27590  wwlksn  27615  wspthneq1eq2  27638  wwlksm1edg  27659  wwlksnred  27670  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextproplem3  27690  wspthsnonn0vne  27696  wspn0  27703  rusgrnumwwlk  27754  clwwlkccatlem  27767  umgrclwwlkge2  27769  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  clwwisshclwws  27793  clwwisshclwwsn  27794  clwwlkn1loopb  27821  clwwlknfiOLD  27824  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  clwwlknonex2lem2  27887  upgr3v3e3cycl  27959  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  eupth2lem3lem4  28010  eupth2lem3lem7  28013  eupth2  28018  eulerpath  28020  nfrgr2v  28051  frgr3vlem1  28052  3vfriswmgr  28057  1to2vfriswmgr  28058  1to3vfriswmgr  28059  3cyclfrgrrn1  28064  3cyclfrgrrn  28065  3cyclfrgrrn2  28066  4cycl2vnunb  28069  frgrncvvdeqlem2  28079  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  frgrwopreglem4a  28089  frgrwopreglem5lem  28099  frgrwopreglem5ALT  28101  frgrregorufr0  28103  frgr2wwlk1  28108  frgr2wwlkeqm  28110  fusgr2wsp2nb  28113  2wspmdisj  28116  frrusgrord  28120  numclwwlk1lem2f1  28136  numclwlk1  28150  frgrreggt1  28172  friendshipgt3  28177  hlim2  28969  elnlfn  29705  stle0i  30016  hstrbi  30043  spansncv2  30070  h1da  30126  fmptcof2  30402  xreceu  30598  tpr2rico  31155  hasheuni  31344  ismeas  31458  sseqp1  31653  rrvsum  31712  dstfrvunirn  31732  sgn3da  31799  signstfvc  31844  bnj607  32188  bnj1145  32265  bnj1204  32284  fisshasheq  32352  subgrwlk  32379  subfacp1lem6  32432  cvmlift2lem12  32561  cvmlift3lem4  32569  satfrnmapom  32617  sat1el2xp  32626  satffunlem2  32655  satffun  32656  mrsubvrs  32769  climuzcnv  32914  iprodefisumlem  32972  dfon2lem9  33036  trpredtr  33069  trpredmintr  33070  dftrpred3g  33072  trpredrec  33077  soseq  33096  frrlem8  33130  fpr2  33140  frr2  33145  sltval2  33163  sltsolem1  33180  linethru  33614  elhf2  33636  finminlem  33666  fnessref  33705  neibastop2lem  33708  fnemeet2  33715  nndivsub  33805  bj-xpnzex  34274  bj-elpwg  34348  bj-epelg  34363  bj-intss  34394  mptsnunlem  34622  dissneqlem  34624  topdifinffinlem  34631  iooelexlt  34646  domalom  34688  fvineqsneq  34696  wl-exeq  34789  wl-ax11-lem3  34834  matunitlindflem1  34903  poimirlem22  34929  poimirlem26  34933  poimirlem28  34935  poimirlem29  34936  poimirlem32  34939  heicant  34942  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  cover2  35004  upixp  35019  sdclem2  35032  fdc  35035  seqpo  35037  metf1o  35045  mettrifi  35047  sstotbnd3  35069  heibor1lem  35102  heiborlem5  35108  heibor  35114  bfplem1  35115  elghomlem2OLD  35179  grpokerinj  35186  isrngo  35190  rngodm1dm2  35225  ispridl2  35331  exlimddvf  35414  lssatle  36166  4atexlemex4  37224  sn-axprlem3  39158  mzpsubst  39394  jm2.18  39634  wepwsolem  39691  iunrelexp0  40096  relexpmulg  40104  cnvtrclfv  40118  clsk1indlem3  40442  grucollcld  40645  inaex  40682  dvgrat  40693  radcnvrat  40695  csbxpgVD  41277  sineq0ALT  41320  islptre  41949  iblspltprt  42307  stoweidlem2  42336  stoweidlem17  42351  stoweidlem21  42355  2reuimp0  43362  2reuimp  43363  afveu  43401  funbrafv  43406  ndmaovass  43454  afv2eu  43486  tz6.12c-afv2  43490  funop1  43531  f1oresf1o2  43539  fvmptrabdm  43541  nltle2tri  43562  2elfz2melfz  43567  fzoopth  43576  fsummsndifre  43581  fsumsplitsndif  43582  fsummmodsndifre  43583  fsummmodsnunz  43584  elsetpreimafvssdm  43595  uniimaelsetpreimafv  43605  imasetpreimafvbijlemfv1  43612  iccpartiltu  43631  iccpartigtl  43632  iccpartleu  43637  iccpartgel  43638  iccpartrn  43639  iccpartiun  43643  icceuelpart  43645  iccpartnel  43647  fargshiftf  43649  fargshiftf1  43650  ichnfb  43674  elsprel  43686  prsprel  43698  sprsymrelfo  43708  paireqne  43722  sbcpr  43732  reupr  43733  fmtnoinf  43747  odz2prm2pw  43774  lighneallem4  43824  lighneal  43825  requad1  43836  requad2  43837  evensumeven  43921  even3prm2  43933  gbowgt5  43976  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbnnsum3prm  44018  bgoldbtbndlem2  44020  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomuspgrlem1  44041  clcllaw  44147  nrhmzr  44193  rnghmmul  44220  rngccatidALTV  44309  ringccatidALTV  44372  nzerooringczr  44392  scmsuppss  44469  gsumlsscl  44480  ply1mulgsumlem2  44490  lincvalsc0  44525  linc0scn0  44527  lincdifsn  44528  linc1  44529  lincellss  44530  lincsum  44533  lincscm  44534  lincsumcl  44535  lcoss  44540  lincext3  44560  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  lindslinindsimp2  44567  lindsrng01  44572  snlindsntor  44575  lincresunit3lem2  44584  lincresunit3  44585  islindeps2  44587  blengt1fldiv2p1  44702  resum2sqorgt0  44745  reorelicc  44746  rrx2plordisom  44759  rrx2linest  44778  rrxsphere  44784  line2ylem  44787  itsclc0xyqsol  44804  itscnhlinecirc02p  44821