Theorem expcom 413

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancoms  458  pm3.21  471  sylan  581  animpimp2impd  847  4casesdan  1042  dedlema  1046  dedlemb  1047  sbiedvw  2101  mo4  2567  2moswapv  2630  2moswap  2645  2mosOLD  2651  2eu2  2654  pm2.61ne  3018  nelelne  3032  r19.21be  3231  cbvraldva2  3320  rspcebdv  3572  2reu2  3850  csbie2df  4397  minel  4420  uneqdifeq  4447  raltpd  4740  ssunsn2  4785  opthprneg  4823  ssuni  4890  uniss2  4899  elpwuni  5062  intss2  5065  disjord  5089  elpw2g  5282  elssabg  5292  axprlem3OLD  5377  axprlem4OLD  5378  axprlem5OLD  5379  axprglem  5384  oteqex  5458  otsndisj  5477  otiunsndisj  5478  epelg  5535  wereu  5630  relop  5809  riinint  5931  sotri3  6097  unixpid  6252  reuop  6261  ordtr2  6372  ordsssuc2  6420  iotan0  6492  funopg  6536  fun  6706  fvmptnf  6974  fvn0ssdmfun  7030  eldmrexrnb  7048  fmptco  7086  fnressn  7115  fressnfv  7117  fprb  7152  fvtp2g  7157  fvtp3g  7158  fconst2g  7161  fntpb  7167  f1dom3el3dif  7227  f1ounsn  7230  isores3  7293  isoselem  7299  oprabv  7430  eloprabga  7479  sorpsscmpl  7691  difex2  7717  ordpwsuc  7769  ordsucun  7779  limuni3  7806  trom  7829  fo1stres  7971  poxp  8082  soxp  8083  xpord3inddlem  8108  soseq  8113  suppimacnv  8128  fsuppeq  8129  funsssuppss  8144  brtpos2  8186  frrlem8  8247  fpr2a  8256  onnseq  8288  smores  8296  smofvon2  8300  tfrlem1  8319  oacl  8474  omcl  8475  oecl  8476  oawordri  8489  oalimcl  8499  oaass  8500  oarec  8501  omwordri  8511  omeulem1  8521  omeulem2  8522  oeordi  8527  oeworde  8533  oeoelem  8538  nnacl  8551  nnmcl  8552  nnecl  8553  nnacom  8557  nnaass  8562  nnmsucr  8565  nnmordi  8571  omabs  8591  cofonr  8614  naddunif  8633  iiner  8740  elpmg  8794  fsetfcdm  8811  fsetprcnex  8813  pmss12g  8821  mapfvd  8831  f1domg  8922  ssdomg  8951  undom  9007  domtriord  9065  ssnnfi  9108  fnfi  9116  enfi  9125  php  9145  sdom1  9164  1sdom2dom  9168  fisseneq  9177  isinf  9179  dif1ennnALT  9191  findcard3  9197  frfi  9199  difinf  9225  imafiOLD  9230  iunfi  9257  fsuppunfi  9305  fsuppres  9310  ffsuppbi  9315  elfi2  9331  marypha1lem  9350  marypha1  9351  oiexg  9454  wemapso2  9472  harword  9482  brwdom  9486  unxpwdom  9508  en3lplem1  9535  inf3lemd  9550  inf3lem5  9555  cantnfval2  9592  cantnfle  9594  cantnflt  9595  cnfcom  9623  tcmin  9662  frr2  9686  r1sdom  9700  rankxplim3  9807  cardidm  9885  cardmin2  9925  infxpenlem  9937  fseqenlem1  9948  numacn  9973  alephordi  9998  iscard3  10017  alephinit  10019  carduniima  10020  iunfictbso  10038  dfac5  10053  dfac12lem3  10070  nnadju  10122  pwsdompw  10127  pwdjudom  10139  cflim2  10187  cfslb2n  10192  cofsmo  10193  cfsmolem  10194  cfcoflem  10196  alephsing  10200  infpssALT  10237  fin23lem34  10270  isf32lem2  10278  isf32lem10  10286  isf32lem12  10288  isfin1-2  10309  hsmexlem4  10353  axcc2lem  10360  domtriomlem  10366  axdc2lem  10372  axdc3lem2  10375  axdc3lem4  10377  axdc4lem  10379  axcclem  10381  ac6num  10403  ac6s  10408  zorn2lem7  10426  ttukeylem5  10437  imadomg  10458  iundom2g  10464  ondomon  10487  ficard  10489  konigthlem  10493  alephreg  10507  pwcfsdom  10508  cfpwsdom  10509  axregndlem1  10527  axregnd  10529  pwfseqlem3  10585  pwxpndom2  10590  pwxpndom  10591  pwdjundom  10592  inawinalem  10614  gchina  10624  wuncval2  10672  tsk0  10688  tskxpss  10697  inatsk  10703  tskuni  10708  gruina  10743  grothac  10755  addclpi  10817  addnidpi  10826  nqereu  10854  mulcanenq  10885  genpnnp  10930  nqpr  10939  prlem934  10958  reclem2pr  10973  suplem1pr  10977  supsrlem  11036  axpre-sup  11094  1re  11146  dedekindle  11311  00id  11322  receu  11796  sup3  12113  infrelb  12141  peano5nni  12162  nnindd  12179  nnaddcl  12182  zrevaddcl  12550  nzadd  12553  zdiv  12576  nneo  12590  zeo2  12593  nn0indd  12603  fzind  12604  fnn0ind  12605  fzindd  12608  uzwo  12838  lbzbi  12863  nn01to3  12868  qrevaddcl  12898  irradd  12900  irrmul  12901  ltsubrp  12957  ltaddrp  12958  xnn0xaddcl  13164  xnn0xadd0  13176  icoshft  13403  fzen  13471  elfzm11  13525  uzsplit  13526  elfzom1elp1fzo  13662  fzoopth  13692  injresinjlem  13720  injresinj  13721  modifeq2int  13870  modsumfzodifsn  13881  om2uzlti  13887  ssnn0fi  13922  fsuppmapnn0fiub0  13930  mptnn0fsuppr  13936  seqcaopr3  13974  seqf1olem2a  13977  seqf1o  13980  ser1const  13995  expadd  14041  expmul  14044  leexp1a  14112  faccl  14220  facdiv  14224  faclbnd  14227  faclbnd4lem4  14233  hasheqf1oi  14288  hashgadd  14314  hashinfxadd  14322  hashunx  14323  hashunsng  14329  elprchashprn2  14333  hashss  14346  hash1snb  14356  hashmap  14372  hashf1lem2  14393  hashf1  14394  seqcoll  14401  hashle2pr  14414  hashdmpropge2  14420  hashge3el3dif  14424  hash1to3  14429  fundmge2nop0  14439  fi1uzind  14444  brfi1indALT  14447  sswrd  14459  swrdnd2  14593  swrdnnn0nd  14594  swrdnd0  14595  swrdwrdsymb  14600  pfxnd0  14626  swrdswrdlem  14641  swrdswrd  14642  wrd2ind  14660  swrdccatin1  14662  swrdccatin2  14666  pfxccatin12lem2  14668  pfxccat3  14671  repsdf2  14715  repswswrd  14721  cshw0  14731  cshwcl  14735  cshwlen  14736  cshf1  14747  swrdco  14774  relexpsucnnl  14967  rtrclreclem3  14997  rtrclreclem4  14998  relexpindlem  15000  rtrclind  15002  shftlem  15005  caubnd  15296  reusq0  15402  rlimcld2  15515  o1dif  15567  climub  15599  climserle  15600  iseraltlem2  15620  sumss  15661  fsumzcl2  15676  fsummsnunz  15691  fsumsplitsnun  15692  fsum2d  15708  modfsummods  15730  fsumabs  15738  fsumrlim  15748  fsumo1  15749  fsumiun  15758  climcndslem1  15786  climcndslem2  15787  cvgrat  15820  clim2prod  15825  prodfn0  15831  prodfrec  15832  ntrivcvg  15834  prodmo  15873  fprodss  15885  fprodabs  15911  fprodn0  15916  fprod2d  15918  fprodefsum  16032  ruclem8  16176  ruclem9  16177  dvdsmod0  16199  dvds2ln  16230  dvdsaddre2b  16248  dvdslelem  16250  dvdsdivcl  16257  alzdvds  16261  mod2eq1n2dvds  16288  oddnn02np1  16289  nn0o1gt2  16322  nno  16323  sumeven  16328  sumodd  16329  pwp1fsum  16332  ndvdsadd  16351  bitsinv1  16383  sadcadd  16399  sadadd2  16401  saddisjlem  16405  smuval2  16423  smupvallem  16424  smu01lem  16426  smupval  16429  smueqlem  16431  smumullem  16433  gcddiv  16492  rplpwr  16499  nn0seqcvgd  16511  seq1st  16512  alginv  16516  algcvga  16520  algfx  16521  absprodnn  16559  isprm2  16623  isprm3  16624  prmind2  16626  maxprmfct  16650  prmdvdsexp  16656  pcmpt  16834  prmreclem4  16861  vdwmc2  16921  vdwlem10  16932  ramub2  16956  ramcl  16971  prmgaplem5  16997  prmgaplem8  17000  cshwshashlem1  17037  cshwshashlem3  17039  setsn0fun  17114  imasleval  17476  divsfval  17482  mreexexlem4d  17584  isssc  17758  initoeu1  17949  termoeu1  17956  istos  18353  chnfibg  18573  mgmcl  18582  sgrpidmnd  18678  frmdgsum  18801  smndex1mgm  18849  dfgrp3lem  18985  mhmmulg  19062  resghm2b  19180  gsumwrev  19312  elsymgbas  19320  symgextf1  19367  gsmsymgreqlem2  19377  gsmsymgreq  19378  odlem1  19481  odcl2  19511  gexlem1  19525  efgi2  19671  efginvrel2  19673  efgsrel  19680  cyggexb  19845  gsummulglem  19887  gsumzunsnd  19902  gsum2dlem2  19917  telgsums  19939  dmdprd  19946  dprdw  19958  ablfac1eulem  20020  srgpcomp  20170  rnghmmul  20402  nrhmzr  20487  lmodfopnelem1  20866  rmodislmodlem  20897  cnfldmulg  21375  cnfldexp  21376  nzerooringczr  21452  obslbs  21702  mplcoe1  22009  mplcoe3  22010  mplcoe5  22012  cply1mul  22257  coe1fzgsumdlem  22264  gsummoncoe1  22269  pf1ind  22316  evl1gsumdlem  22317  mat1dimcrng  22438  ma1repveval  22532  mulmarep1gsum2  22535  gsummatr01lem3  22618  cramerlem3  22650  decpmatmulsumfsupp  22734  mp2pm2mplem4  22770  pm2mpmhmlem1  22779  fvmptnn04if  22810  cayhamlem1  22827  fctop  22965  mretopd  23053  restopnb  23136  restdis  23139  tgcnp  23214  cncls2  23234  cncls  23235  cnntr  23236  cnsscnp  23240  cmpsub  23361  2ndcsep  23420  1stcelcls  23422  lfinpfin  23485  locfincmp  23487  comppfsc  23493  txcn  23587  txlm  23609  xkohaus  23614  qtopres  23659  haushmphlem  23748  cmphmph  23749  connhmph  23750  reghmph  23754  nrmhmph  23755  ptcmpfi  23774  reghaus  23786  fbssfi  23798  fbun  23801  fbfinnfr  23802  isfildlem  23818  fgcl  23839  cfinfil  23854  supfil  23856  ufinffr  23890  fin1aufil  23893  cnpflf  23962  alexsubALTlem3  24010  alexsubALT  24012  cnextfvval  24026  cnextcn  24028  tmdgsum  24056  tgphaus  24078  tgpt1  24079  mettri  24313  blssexps  24387  blssex  24388  mopni3  24455  metss  24469  psmetutop  24528  dscmet  24533  tngngp3  24617  rectbntr0  24794  metnrmlem1a  24820  fsumcn  24834  lmmbr  25231  caubl  25281  caublcls  25282  bcthlem5  25301  bcth3  25304  ovolunlem1a  25470  ovoliunnul  25481  finiunmbl  25518  voliunlem1  25524  volsuplem  25529  volsup  25530  dyadmax  25572  itgfsum  25801  dvnadd  25904  cpnord  25910  dvnfre  25929  dvmptfsum  25952  dvlip  25971  fta1g  26148  plyco  26219  dgrcolem1  26252  dgrco  26254  dvnply2  26268  plydivex  26278  plyexmo  26294  aannenlem1  26309  aaliou3lem2  26324  dvntaylp  26352  taylthlem1  26354  ulmval  26362  cxpmul2  26671  cxpsqrtth  26712  scvxcvx  26969  jensenlem2  26971  jensen  26972  ppiub  27188  bcmono  27261  bpos1lem  27266  bposlem5  27272  gausslemma2dlem6  27356  lgsquad2lem2  27369  2lgslem3  27388  2lgs  27391  2sqnn  27423  addsqnreup  27427  2sqreultblem  27432  2sqreunnltblem  27435  dchrisumlem1  27473  dchrisum0flb  27494  pntpbnd1  27570  pntlemf  27589  qabvle  27609  qabvexp  27610  ostthlem2  27612  ostth2lem2  27618  ltsval2  27641  ltssolem1  27660  negsprop  28048  mulsuniflem  28162  precsexlem6  28225  precsexlem7  28226  noseqind  28305  om2noseqlt  28312  n0addscl  28357  n0mulscl  28358  expsne0  28449  axeuclidlem  29053  axcontlem12  29066  umgrnloopv  29197  uhgredgrnv  29221  edglnl  29234  numedglnl  29235  usgruspgrb  29274  usgrnloopvALT  29292  usgredg2vlem2  29317  subupgr  29378  nbumgr  29438  uhgrnbgr0nb  29445  nbgr0edglem  29447  edgusgrnbfin  29464  nb3grprlem2  29472  uvtxnbgrvtx  29484  cplgrop  29528  cusgrfi  29550  fusgrmaxsize  29556  fusgrn0degnn0  29591  ewlkprop  29695  uspgr2wlkeq  29737  g0wlk0  29742  wlkreslem  29759  lfgriswlk  29778  upgrwlkdvde  29828  spthonepeq  29843  uhgrwkspth  29846  usgr2trlncl  29851  usgr2trlspth  29852  cyclnumvtx  29891  cyclnspth  29892  crctcshwlkn0lem3  29903  wwlksn  29928  wspthneq1eq2  29951  wwlksm1edg  29972  wwlksnred  29983  wwlksnextfun  29989  wwlksnextinj  29990  wwlksnextproplem3  30002  wspthsnonn0vne  30008  wspn0  30015  rusgrnumwwlk  30069  clwwlkccatlem  30082  umgrclwwlkge2  30084  clwlkclwwlklem2  30093  clwlkclwwlklem3  30094  clwwisshclwws  30108  clwwisshclwwsn  30109  clwwlkn1loopb  30136  wwlksext2clwwlk  30150  wwlksubclwwlk  30151  clwwlknonex2lem2  30201  upgr3v3e3cycl  30273  uhgr3cyclex  30275  upgr4cycl4dv4e  30278  eupth2lem3lem4  30324  eupth2lem3lem7  30327  eupth2  30332  eulerpath  30334  nfrgr2v  30365  frgr3vlem1  30366  3vfriswmgr  30371  1to2vfriswmgr  30372  1to3vfriswmgr  30373  3cyclfrgrrn1  30378  3cyclfrgrrn  30379  3cyclfrgrrn2  30380  4cycl2vnunb  30383  frgrncvvdeqlem2  30393  frgrncvvdeqlem8  30399  frgrncvvdeqlem9  30400  frgrwopreglem4a  30403  frgrwopreglem5lem  30413  frgrwopreglem5ALT  30415  frgrregorufr0  30417  frgr2wwlk1  30422  frgr2wwlkeqm  30424  fusgr2wsp2nb  30427  2wspmdisj  30430  frrusgrord  30434  numclwwlk1lem2f1  30450  numclwlk1  30464  frgrreggt1  30486  friendshipgt3  30491  hlim2  31286  elnlfn  32022  stle0i  32333  hstrbi  32360  spansncv2  32387  h1da  32443  fmptcof2  32753  sgn3da  32932  xreceu  33020  domnprodn0  33375  1arithufdlem3  33645  1arithufdlem4  33646  tpr2rico  34096  hasheuni  34269  ismeas  34383  sseqp1  34579  rrvsum  34638  dstfrvunirn  34659  signstfvc  34758  bnj607  35098  bnj1145  35175  bnj1204  35194  r1filim  35287  fineqvrep  35298  fineqvnttrclselem1  35305  onvf1odlem4  35328  fisshasheq  35337  subgrwlk  35354  subfacp1lem6  35407  cvmlift2lem12  35536  cvmlift3lem4  35544  satfrnmapom  35592  sat1el2xp  35601  satffunlem2  35630  satffun  35631  mrsubvrs  35744  climuzcnv  35893  iprodefisumlem  35962  dfon2lem9  36011  linethru  36375  elhf2  36397  finminlem  36540  fnessref  36579  neibastop2lem  36582  fnemeet2  36589  nndivsub  36679  bj-cbvew  36904  bj-xpnzex  37234  bj-elpwg  37327  bj-epelg  37343  bj-axseprep  37349  mptsnunlem  37620  dissneqlem  37622  topdifinffinlem  37629  iooelexlt  37644  domalom  37686  fvineqsneq  37694  wl-exeq  37818  matunitlindflem1  37896  poimirlem22  37922  poimirlem26  37926  poimirlem28  37928  poimirlem29  37929  poimirlem32  37932  heicant  37935  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  cover2  37995  upixp  38009  sdclem2  38022  fdc  38025  seqpo  38027  metf1o  38035  mettrifi  38037  sstotbnd3  38056  heibor1lem  38089  heiborlem5  38095  heibor  38101  bfplem1  38102  elghomlem2OLD  38166  grpokerinj  38173  isrngo  38177  rngodm1dm2  38212  ispridl2  38318  exlimddvf  38401  lssatle  39420  4atexlemex4  40478  uzindd  42376  evl1gprodd  42516  sn-axprlem3  42619  redvmptabs  42759  sn-sup3d  42891  mzpsubst  43134  jm2.18  43374  wepwsolem  43428  oaabsb  43680  oacl2g  43716  ofoafg  43740  ofoaid1  43744  ofoaid2  43745  naddonnn  43781  iunrelexp0  44087  relexpmulg  44095  cnvtrclfv  44109  clsk1indlem3  44428  grucollcld  44645  inaex  44682  dvgrat  44697  radcnvrat  44699  csbxpgVD  45278  sineq0ALT  45321  trfr  45347  relwf  45352  pwclaxpow  45369  omssaxinf2  45373  islptre  46008  iblspltprt  46360  stoweidlem2  46389  stoweidlem17  46404  stoweidlem21  46408  2reuimp0  47503  2reuimp  47504  afveu  47542  funbrafv  47547  ndmaovass  47595  afv2eu  47627  tz6.12c-afv2  47631  funop1  47672  f1oresf1o2  47680  fvmptrabdm  47682  nltle2tri  47702  2elfz2melfz  47707  fsummsndifre  47761  fsumsplitsndif  47762  fsummmodsndifre  47763  fsummmodsnunz  47764  elsetpreimafvssdm  47775  uniimaelsetpreimafv  47785  imasetpreimafvbijlemfv1  47792  iccpartiltu  47811  iccpartigtl  47812  iccpartleu  47817  iccpartgel  47818  iccpartrn  47819  iccpartiun  47823  icceuelpart  47825  iccpartnel  47827  fargshiftf  47829  fargshiftf1  47830  ichnfb  47854  elsprel  47864  prsprel  47876  sprsymrelfo  47886  paireqne  47900  sbcpr  47910  reupr  47911  fmtnoinf  47925  odz2prm2pw  47952  lighneallem4  47999  lighneal  48000  requad1  48011  requad2  48012  evensumeven  48096  even3prm2  48108  gbowgt5  48151  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  bgoldbnnsum3prm  48193  bgoldbtbndlem2  48195  bgoldbtbndlem4  48197  bgoldbtbnd  48198  dfsclnbgr6  48247  grimco  48278  cycl3grtri  48336  isubgr3stgrlem6  48360  gricgrlic  48407  gpgedgvtx0  48450  gpgprismgr4cycllem3  48486  pgnbgreunbgrlem5  48512  clcllaw  48580  rngccatidALTV  48661  ringccatidALTV  48695  scmsuppss  48760  gsumlsscl  48769  ply1mulgsumlem2  48776  lincvalsc0  48810  linc0scn0  48812  lincdifsn  48813  linc1  48814  lincellss  48815  lincsum  48818  lincscm  48819  lincsumcl  48820  lcoss  48825  lincext3  48845  lindslinindimp2lem4  48850  lindslinindsimp2lem5  48851  lindslinindsimp2  48852  lindsrng01  48857  snlindsntor  48860  lincresunit3lem2  48869  lincresunit3  48870  islindeps2  48872  blengt1fldiv2p1  48982  2arymaptf1  49042  resum2sqorgt0  49098  reorelicc  49099  rrx2plordisom  49112  rrx2linest  49131  rrxsphere  49137  line2ylem  49140  itsclc0xyqsol  49157  itscnhlinecirc02p  49174  mo0sn  49204  thincn0eu  49819