Theorem expcom 415

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ancoms  460  pm3.21  473  sylan  581  animpimp2impd  845  4casesdan  1041  dedlema  1045  dedlemb  1046  sbiedvw  2097  mo4  2561  2moswapv  2626  2moswap  2641  2mos  2646  2eu2  2649  pm2.61ne  3028  nelelne  3042  r19.21be  3250  cbvraldva2  3345  rspcebdv  3607  2reu2  3893  csbie2df  4441  minel  4466  uneqdifeq  4493  raltpd  4786  ssunsn2  4831  opthprneg  4866  ssuni  4937  uniss2  4946  elpwuni  5109  intss2  5112  disjord  5137  elssabg  5337  elpw2g  5345  axprlem3  5424  axprlem4  5425  axprlem5  5426  oteqex  5501  otsndisj  5520  otiunsndisj  5521  epelg  5582  wereu  5673  relop  5851  riinint  5968  sotri3  6132  unixpid  6284  reuop  6293  ordtr2  6409  ordsssuc2  6456  iotan0  6534  funopg  6583  fun  6754  tz6.12cOLD  6919  fvmptnf  7021  fvn0ssdmfun  7077  eldmrexrnb  7094  fmptco  7127  fnressn  7156  fressnfv  7158  fprb  7195  fvtp2g  7200  fvtp3g  7201  fconst2g  7204  fntpb  7211  f1dom3el3dif  7268  isores3  7332  isoselem  7338  oprabv  7469  eloprabga  7516  eloprabgaOLD  7517  sorpsscmpl  7724  difex2  7747  ordpwsuc  7803  ordsucun  7813  limuni3  7841  trom  7864  fo1stres  8001  poxp  8114  soxp  8115  xpord3inddlem  8140  soseq  8145  suppimacnv  8159  fsuppeq  8160  funsssuppss  8175  brtpos2  8217  frrlem8  8278  fpr2a  8287  wfrlem12OLD  8320  onnseq  8344  smores  8352  smofvon2  8356  tfrlem1  8376  oacl  8535  omcl  8536  oecl  8537  oawordri  8550  oalimcl  8560  oaass  8561  oarec  8562  omwordri  8572  omeulem1  8582  omeulem2  8583  oeordi  8587  oeworde  8593  oeoelem  8598  nnacl  8611  nnmcl  8612  nnecl  8613  nnacom  8617  nnaass  8622  nnmsucr  8625  nnmordi  8631  omabs  8650  cofonr  8673  naddunif  8692  iiner  8783  elpmg  8837  fsetfcdm  8854  fsetprcnex  8856  pmss12g  8863  mapfvd  8873  f1domg  8968  ssdomg  8996  undom  9059  domtriord  9123  ssnnfi  9169  ssnnfiOLD  9170  imafi  9175  fnfi  9181  enfi  9190  php  9210  phpOLD  9222  php3OLD  9224  sdom1  9242  1sdom2dom  9247  1sdomOLD  9249  fisseneq  9257  isinf  9260  isinfOLD  9261  dif1ennnALT  9277  findcard3  9285  findcard3OLD  9286  frfi  9288  unfiOLD  9313  difinf  9316  iunfi  9340  fsuppunfi  9383  fsuppres  9388  ffsuppbi  9393  elfi2  9409  marypha1lem  9428  marypha1  9429  oiexg  9530  wemapso2  9548  harword  9558  brwdom  9562  unxpwdom  9584  en3lplem1  9607  inf3lemd  9622  inf3lem5  9627  cantnfval2  9664  cantnfle  9666  cantnflt  9667  cnfcom  9695  tcmin  9736  frr2  9755  r1sdom  9769  rankxplim3  9876  cardidm  9954  cardmin2  9994  infxpenlem  10008  fseqenlem1  10019  numacn  10044  alephordi  10069  iscard3  10088  alephinit  10090  carduniima  10091  iunfictbso  10109  dfac5  10123  dfac12lem3  10140  nnadju  10192  pwsdompw  10199  pwdjudom  10211  cflim2  10258  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  alephsing  10271  infpssALT  10308  fin23lem34  10341  isf32lem2  10349  isf32lem10  10357  isf32lem12  10359  isfin1-2  10380  hsmexlem4  10424  axcc2lem  10431  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  ac6num  10474  ac6s  10479  zorn2lem7  10497  ttukeylem5  10508  imadomg  10529  iundom2g  10535  ondomon  10558  ficard  10560  konigthlem  10563  alephreg  10577  pwcfsdom  10578  cfpwsdom  10579  axregndlem1  10597  axregnd  10599  pwfseqlem3  10655  pwxpndom2  10660  pwxpndom  10661  pwdjundom  10662  inawinalem  10684  gchina  10694  wuncval2  10742  tsk0  10758  tskxpss  10767  inatsk  10773  tskuni  10778  gruina  10813  grothac  10825  addclpi  10887  addnidpi  10896  nqereu  10924  mulcanenq  10955  genpnnp  11000  nqpr  11009  prlem934  11028  reclem2pr  11043  suplem1pr  11047  supsrlem  11106  axpre-sup  11164  1re  11214  dedekindle  11378  00id  11389  receu  11859  sup3  12171  infrelb  12199  peano5nni  12215  nnindd  12232  nnaddcl  12235  zrevaddcl  12607  nzadd  12610  zdiv  12632  nneo  12646  zeo2  12649  nn0indd  12659  fzind  12660  fnn0ind  12661  fzindd  12664  uzwo  12895  lbzbi  12920  nn01to3  12925  qrevaddcl  12955  irradd  12957  irrmul  12958  ltsubrp  13010  ltaddrp  13011  xnn0xaddcl  13214  xnn0xadd0  13226  icoshft  13450  fzen  13518  elfzm11  13572  uzsplit  13573  elfzoext  13689  elfzom1elp1fzo  13699  injresinjlem  13752  injresinj  13753  modifeq2int  13898  modsumfzodifsn  13909  om2uzlti  13915  ssnn0fi  13950  fsuppmapnn0fiub0  13958  mptnn0fsuppr  13964  seqcaopr3  14003  seqf1olem2a  14006  seqf1o  14009  ser1const  14024  expadd  14070  expmul  14073  leexp1a  14140  faccl  14243  facdiv  14247  faclbnd  14250  faclbnd4lem4  14256  hasheqf1oi  14311  hashgadd  14337  hashinfxadd  14345  hashunx  14346  hashunsng  14352  elprchashprn2  14356  hashss  14369  hash1snb  14379  hashmap  14395  hashf1lem2  14417  hashf1  14418  seqcoll  14425  hashle2pr  14438  hashdmpropge2  14444  hashge3el3dif  14447  hash1to3  14452  fundmge2nop0  14453  fi1uzind  14458  brfi1indALT  14461  sswrd  14472  swrdnd2  14605  swrdnnn0nd  14606  swrdnd0  14607  swrdwrdsymb  14612  pfxnd0  14638  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccat3  14684  repsdf2  14728  repswswrd  14734  cshw0  14744  cshwcl  14748  cshwlen  14749  cshf1  14760  swrdco  14788  relexpsucnnl  14977  rtrclreclem3  15007  rtrclreclem4  15008  relexpindlem  15010  rtrclind  15012  shftlem  15015  caubnd  15305  reusq0  15409  rlimcld2  15522  o1dif  15574  climub  15608  climserle  15609  iseraltlem2  15629  sumss  15670  fsumzcl2  15685  fsummsnunz  15700  fsumsplitsnun  15701  fsum2d  15717  modfsummods  15739  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  climcndslem1  15795  climcndslem2  15796  cvgrat  15829  clim2prod  15834  prodfn0  15840  prodfrec  15841  ntrivcvg  15843  prodmo  15880  fprodss  15892  fprodabs  15918  fprodn0  15923  fprod2d  15925  fprodefsum  16038  ruclem8  16180  ruclem9  16181  dvdsmod0  16203  dvds2ln  16232  dvdsaddre2b  16250  dvdslelem  16252  dvdsdivcl  16259  alzdvds  16263  mod2eq1n2dvds  16290  oddnn02np1  16291  nn0o1gt2  16324  nno  16325  sumeven  16330  sumodd  16331  pwp1fsum  16334  ndvdsadd  16353  bitsinv1  16383  sadcadd  16399  sadadd2  16401  saddisjlem  16405  smuval2  16423  smupvallem  16424  smu01lem  16426  smupval  16429  smueqlem  16431  smumullem  16433  gcddiv  16493  rplpwr  16499  nn0seqcvgd  16507  seq1st  16508  alginv  16512  algcvga  16516  algfx  16517  absprodnn  16555  isprm2  16619  isprm3  16620  prmind2  16622  maxprmfct  16646  prmdvdsexp  16652  pcmpt  16825  prmreclem4  16852  vdwmc2  16912  vdwlem10  16923  ramub2  16947  ramcl  16962  prmgaplem5  16988  prmgaplem8  16991  cshwshashlem1  17029  cshwshashlem3  17031  setsn0fun  17106  imasleval  17487  divsfval  17493  mreexexlem4d  17591  isssc  17767  initoeu1  17961  termoeu1  17968  istos  18371  mgmcl  18564  sgrpidmnd  18630  frmdgsum  18743  smndex1mgm  18788  dfgrp3lem  18921  mhmmulg  18995  resghm2b  19110  gsumwrev  19233  elsymgbas  19241  symgextf1  19289  gsmsymgreqlem2  19299  gsmsymgreq  19300  odlem1  19403  odcl2  19433  gexlem1  19447  efgi2  19593  efginvrel2  19595  efgsrel  19602  cyggexb  19767  gsummulglem  19809  gsumzunsnd  19824  gsum2dlem2  19839  telgsums  19861  dmdprd  19868  dprdw  19880  ablfac1eulem  19942  srgpcomp  20041  lmodfopnelem1  20508  rmodislmodlem  20539  cnfldmulg  20977  cnfldexp  20978  obslbs  21285  mplcoe1  21592  mplcoe3  21593  mplcoe5  21595  cply1mul  21818  coe1fzgsumdlem  21825  gsummoncoe1  21828  pf1ind  21874  evl1gsumdlem  21875  mat1dimcrng  21979  ma1repveval  22073  mulmarep1gsum2  22076  gsummatr01lem3  22159  cramerlem3  22191  decpmatmulsumfsupp  22275  mp2pm2mplem4  22311  pm2mpmhmlem1  22320  fvmptnn04if  22351  cayhamlem1  22368  fctop  22507  mretopd  22596  restopnb  22679  restdis  22682  tgcnp  22757  cncls2  22777  cncls  22778  cnntr  22779  cnsscnp  22783  cmpsub  22904  2ndcsep  22963  1stcelcls  22965  lfinpfin  23028  locfincmp  23030  comppfsc  23036  txcn  23130  txlm  23152  xkohaus  23157  qtopres  23202  haushmphlem  23291  cmphmph  23292  connhmph  23293  reghmph  23297  nrmhmph  23298  ptcmpfi  23317  reghaus  23329  fbssfi  23341  fbun  23344  fbfinnfr  23345  isfildlem  23361  fgcl  23382  cfinfil  23397  supfil  23399  ufinffr  23433  fin1aufil  23436  cnpflf  23505  alexsubALTlem3  23553  alexsubALT  23555  cnextfvval  23569  cnextcn  23571  tmdgsum  23599  tgphaus  23621  tgpt1  23622  mettri  23858  blssexps  23932  blssex  23933  mopni3  24003  metss  24017  psmetutop  24076  dscmet  24081  tngngp3  24173  rectbntr0  24348  metnrmlem1a  24374  fsumcn  24386  lmmbr  24775  caubl  24825  caublcls  24826  bcthlem5  24845  bcth3  24848  ovolunlem1a  25013  ovoliunnul  25024  finiunmbl  25061  voliunlem1  25067  volsuplem  25072  volsup  25073  dyadmax  25115  itgfsum  25344  dvnadd  25446  cpnord  25452  dvnfre  25469  dvmptfsum  25492  dvlip  25510  fta1g  25685  plyco  25755  dgrcolem1  25787  dgrco  25789  dvnply2  25800  plydivex  25810  plyexmo  25826  aannenlem1  25841  aaliou3lem2  25856  dvntaylp  25883  taylthlem1  25885  ulmval  25892  cxpmul2  26197  cxpsqrtth  26238  scvxcvx  26490  jensenlem2  26492  jensen  26493  ppiub  26707  bcmono  26780  bpos1lem  26785  bposlem5  26791  gausslemma2dlem6  26875  lgsquad2lem2  26888  2lgslem3  26907  2lgs  26910  2sqnn  26942  addsqnreup  26946  2sqreultblem  26951  2sqreunnltblem  26954  dchrisumlem1  26992  dchrisum0flb  27013  pntpbnd1  27089  pntlemf  27108  qabvle  27128  qabvexp  27129  ostthlem2  27131  ostth2lem2  27137  sltval2  27159  sltsolem1  27178  negsprop  27512  mulsuniflem  27607  precsexlem6  27661  precsexlem7  27662  axeuclidlem  28251  axcontlem12  28264  umgrnloopv  28397  uhgredgrnv  28421  edglnl  28434  numedglnl  28435  usgruspgrb  28472  usgrnloopvALT  28489  usgredg2vlem2  28514  subupgr  28575  nbumgr  28635  uhgrnbgr0nb  28642  nbgr0vtxlem  28643  edgusgrnbfin  28661  nb3grprlem2  28669  uvtxnbgrvtx  28681  cplgrop  28725  cusgrfi  28746  fusgrmaxsize  28752  fusgrn0degnn0  28787  ewlkprop  28891  uspgr2wlkeq  28934  g0wlk0  28940  wlkreslem  28957  lfgriswlk  28976  upgrwlkdvde  29025  spthonepeq  29040  uhgrwkspth  29043  usgr2trlncl  29048  usgr2trlspth  29049  cyclnspth  29088  crctcshwlkn0lem3  29097  wwlksn  29122  wspthneq1eq2  29145  wwlksm1edg  29166  wwlksnred  29177  wwlksnextfun  29183  wwlksnextinj  29184  wwlksnextproplem3  29196  wspthsnonn0vne  29202  wspn0  29209  rusgrnumwwlk  29260  clwwlkccatlem  29273  umgrclwwlkge2  29275  clwlkclwwlklem2  29284  clwlkclwwlklem3  29285  clwwisshclwws  29299  clwwisshclwwsn  29300  clwwlkn1loopb  29327  wwlksext2clwwlk  29341  wwlksubclwwlk  29342  clwwlknonex2lem2  29392  upgr3v3e3cycl  29464  uhgr3cyclex  29466  upgr4cycl4dv4e  29469  eupth2lem3lem4  29515  eupth2lem3lem7  29518  eupth2  29523  eulerpath  29525  nfrgr2v  29556  frgr3vlem1  29557  3vfriswmgr  29562  1to2vfriswmgr  29563  1to3vfriswmgr  29564  3cyclfrgrrn1  29569  3cyclfrgrrn  29570  3cyclfrgrrn2  29571  4cycl2vnunb  29574  frgrncvvdeqlem2  29584  frgrncvvdeqlem8  29590  frgrncvvdeqlem9  29591  frgrwopreglem4a  29594  frgrwopreglem5lem  29604  frgrwopreglem5ALT  29606  frgrregorufr0  29608  frgr2wwlk1  29613  frgr2wwlkeqm  29615  fusgr2wsp2nb  29618  2wspmdisj  29621  frrusgrord  29625  numclwwlk1lem2f1  29641  numclwlk1  29655  frgrreggt1  29677  friendshipgt3  29682  hlim2  30476  elnlfn  31212  stle0i  31523  hstrbi  31550  spansncv2  31577  h1da  31633  fmptcof2  31913  xreceu  32119  tpr2rico  32923  hasheuni  33114  ismeas  33228  sseqp1  33425  rrvsum  33484  dstfrvunirn  33504  sgn3da  33571  signstfvc  33616  bnj607  33958  bnj1145  34035  bnj1204  34054  fineqvrep  34126  fisshasheq  34135  subgrwlk  34154  subfacp1lem6  34207  cvmlift2lem12  34336  cvmlift3lem4  34344  satfrnmapom  34392  sat1el2xp  34401  satffunlem2  34430  satffun  34431  mrsubvrs  34544  climuzcnv  34687  iprodefisumlem  34741  dfon2lem9  34794  linethru  35156  elhf2  35178  finminlem  35251  fnessref  35290  neibastop2lem  35293  fnemeet2  35300  nndivsub  35390  bj-xpnzex  35888  bj-elpwg  35981  bj-epelg  35997  mptsnunlem  36267  dissneqlem  36269  topdifinffinlem  36276  iooelexlt  36291  domalom  36333  fvineqsneq  36341  wl-exeq  36451  wl-ax11-lem3  36497  matunitlindflem1  36532  poimirlem22  36558  poimirlem26  36562  poimirlem28  36564  poimirlem29  36565  poimirlem32  36568  heicant  36571  ovoliunnfl  36578  voliunnfl  36580  volsupnfl  36581  cover2  36631  upixp  36645  sdclem2  36658  fdc  36661  seqpo  36663  metf1o  36671  mettrifi  36673  sstotbnd3  36692  heibor1lem  36725  heiborlem5  36731  heibor  36737  bfplem1  36738  elghomlem2OLD  36802  grpokerinj  36809  isrngo  36813  rngodm1dm2  36848  ispridl2  36954  exlimddvf  37037  lssatle  37933  4atexlemex4  38992  uzindd  40890  sn-axprlem3  41082  mzpsubst  41534  jm2.18  41775  wepwsolem  41832  oaabsb  42092  oacl2g  42128  ofoafg  42152  ofoaid1  42156  ofoaid2  42157  naddonnn  42194  iunrelexp0  42501  relexpmulg  42509  cnvtrclfv  42523  clsk1indlem3  42842  grucollcld  43067  inaex  43104  dvgrat  43119  radcnvrat  43121  csbxpgVD  43703  sineq0ALT  43746  islptre  44383  iblspltprt  44737  stoweidlem2  44766  stoweidlem17  44781  stoweidlem21  44785  2reuimp0  45870  2reuimp  45871  afveu  45909  funbrafv  45914  ndmaovass  45962  afv2eu  45994  tz6.12c-afv2  45998  funop1  46039  f1oresf1o2  46047  fvmptrabdm  46049  nltle2tri  46069  2elfz2melfz  46074  fzoopth  46083  fsummsndifre  46088  fsumsplitsndif  46089  fsummmodsndifre  46090  fsummmodsnunz  46091  elsetpreimafvssdm  46102  uniimaelsetpreimafv  46112  imasetpreimafvbijlemfv1  46119  iccpartiltu  46138  iccpartigtl  46139  iccpartleu  46144  iccpartgel  46145  iccpartrn  46146  iccpartiun  46150  icceuelpart  46152  iccpartnel  46154  fargshiftf  46156  fargshiftf1  46157  ichnfb  46181  elsprel  46191  prsprel  46203  sprsymrelfo  46213  paireqne  46227  sbcpr  46237  reupr  46238  fmtnoinf  46252  odz2prm2pw  46279  lighneallem4  46326  lighneal  46327  requad1  46338  requad2  46339  evensumeven  46423  even3prm2  46435  gbowgt5  46478  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  bgoldbnnsum3prm  46520  bgoldbtbndlem2  46522  bgoldbtbndlem4  46524  bgoldbtbnd  46525  isomuspgrlem1  46543  clcllaw  46649  nrhmzr  46695  rnghmmul  46746  rngccatidALTV  46935  ringccatidALTV  46998  nzerooringczr  47018  scmsuppss  47096  gsumlsscl  47107  ply1mulgsumlem2  47116  lincvalsc0  47150  linc0scn0  47152  lincdifsn  47153  linc1  47154  lincellss  47155  lincsum  47158  lincscm  47159  lincsumcl  47160  lcoss  47165  lincext3  47185  lindslinindimp2lem4  47190  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  lindsrng01  47197  snlindsntor  47200  lincresunit3lem2  47209  lincresunit3  47210  islindeps2  47212  blengt1fldiv2p1  47327  2arymaptf1  47387  resum2sqorgt0  47443  reorelicc  47444  rrx2plordisom  47457  rrx2linest  47476  rrxsphere  47482  line2ylem  47485  itsclc0xyqsol  47502  itscnhlinecirc02p  47519  mo0sn  47548  thincn0eu  47700