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  580  animpimp2impd  846  4casesdan  1041  dedlema  1045  dedlemb  1046  sbiedvw  2096  mo4  2559  2moswapv  2622  2moswap  2637  2mosOLD  2643  2eu2  2646  pm2.61ne  3010  nelelne  3024  r19.21be  3222  cbvraldva2  3312  rspcebdv  3573  2reu2  3852  csbie2df  4396  minel  4419  uneqdifeq  4446  raltpd  4735  ssunsn2  4781  opthprneg  4819  ssuni  4886  uniss2  4894  elpwuni  5057  intss2  5060  disjord  5084  elpw2g  5275  elssabg  5285  axprlem3OLD  5370  axprlem4OLD  5371  axprlem5OLD  5372  oteqex  5447  otsndisj  5466  otiunsndisj  5467  epelg  5524  wereu  5619  relop  5797  riinint  5917  sotri3  6083  unixpid  6236  reuop  6245  ordtr2  6356  ordsssuc2  6404  iotan0  6476  funopg  6520  fun  6690  fvmptnf  6956  fvn0ssdmfun  7012  eldmrexrnb  7030  fmptco  7067  fnressn  7096  fressnfv  7098  fprb  7134  fvtp2g  7139  fvtp3g  7140  fconst2g  7143  fntpb  7149  f1dom3el3dif  7210  f1ounsn  7213  isores3  7276  isoselem  7282  oprabv  7413  eloprabga  7462  sorpsscmpl  7674  difex2  7700  ordpwsuc  7754  ordsucun  7764  limuni3  7792  trom  7815  fo1stres  7957  poxp  8068  soxp  8069  xpord3inddlem  8094  soseq  8099  suppimacnv  8114  fsuppeq  8115  funsssuppss  8130  brtpos2  8172  frrlem8  8233  fpr2a  8242  onnseq  8274  smores  8282  smofvon2  8286  tfrlem1  8305  oacl  8460  omcl  8461  oecl  8462  oawordri  8475  oalimcl  8485  oaass  8486  oarec  8487  omwordri  8497  omeulem1  8507  omeulem2  8508  oeordi  8512  oeworde  8518  oeoelem  8523  nnacl  8536  nnmcl  8537  nnecl  8538  nnacom  8542  nnaass  8547  nnmsucr  8550  nnmordi  8556  omabs  8576  cofonr  8599  naddunif  8618  iiner  8723  elpmg  8777  fsetfcdm  8794  fsetprcnex  8796  pmss12g  8803  mapfvd  8813  f1domg  8904  ssdomg  8932  undom  8989  domtriord  9047  ssnnfi  9093  fnfi  9102  enfi  9111  php  9131  sdom1  9149  1sdom2dom  9153  fisseneq  9162  isinf  9165  isinfOLD  9166  dif1ennnALT  9180  findcard3  9187  findcard3OLD  9188  frfi  9190  difinf  9218  imafiOLD  9223  iunfi  9252  fsuppunfi  9297  fsuppres  9302  ffsuppbi  9307  elfi2  9323  marypha1lem  9342  marypha1  9343  oiexg  9446  wemapso2  9464  harword  9474  brwdom  9478  unxpwdom  9500  en3lplem1  9527  inf3lemd  9542  inf3lem5  9547  cantnfval2  9584  cantnfle  9586  cantnflt  9587  cnfcom  9615  tcmin  9656  frr2  9675  r1sdom  9689  rankxplim3  9796  cardidm  9874  cardmin2  9914  infxpenlem  9926  fseqenlem1  9937  numacn  9962  alephordi  9987  iscard3  10006  alephinit  10008  carduniima  10009  iunfictbso  10027  dfac5  10042  dfac12lem3  10059  nnadju  10111  pwsdompw  10116  pwdjudom  10128  cflim2  10176  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  alephsing  10189  infpssALT  10226  fin23lem34  10259  isf32lem2  10267  isf32lem10  10275  isf32lem12  10277  isfin1-2  10298  hsmexlem4  10342  axcc2lem  10349  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  ac6num  10392  ac6s  10397  zorn2lem7  10415  ttukeylem5  10426  imadomg  10447  iundom2g  10453  ondomon  10476  ficard  10478  konigthlem  10481  alephreg  10495  pwcfsdom  10496  cfpwsdom  10497  axregndlem1  10515  axregnd  10517  pwfseqlem3  10573  pwxpndom2  10578  pwxpndom  10579  pwdjundom  10580  inawinalem  10602  gchina  10612  wuncval2  10660  tsk0  10676  tskxpss  10685  inatsk  10691  tskuni  10696  gruina  10731  grothac  10743  addclpi  10805  addnidpi  10814  nqereu  10842  mulcanenq  10873  genpnnp  10918  nqpr  10927  prlem934  10946  reclem2pr  10961  suplem1pr  10965  supsrlem  11024  axpre-sup  11082  1re  11134  dedekindle  11298  00id  11309  receu  11783  sup3  12100  infrelb  12128  peano5nni  12149  nnindd  12166  nnaddcl  12169  zrevaddcl  12538  nzadd  12541  zdiv  12564  nneo  12578  zeo2  12581  nn0indd  12591  fzind  12592  fnn0ind  12593  fzindd  12596  uzwo  12830  lbzbi  12855  nn01to3  12860  qrevaddcl  12890  irradd  12892  irrmul  12893  ltsubrp  12949  ltaddrp  12950  xnn0xaddcl  13155  xnn0xadd0  13167  icoshft  13394  fzen  13462  elfzm11  13516  uzsplit  13517  elfzom1elp1fzo  13653  fzoopth  13683  injresinjlem  13708  injresinj  13709  modifeq2int  13858  modsumfzodifsn  13869  om2uzlti  13875  ssnn0fi  13910  fsuppmapnn0fiub0  13918  mptnn0fsuppr  13924  seqcaopr3  13962  seqf1olem2a  13965  seqf1o  13968  ser1const  13983  expadd  14029  expmul  14032  leexp1a  14100  faccl  14208  facdiv  14212  faclbnd  14215  faclbnd4lem4  14221  hasheqf1oi  14276  hashgadd  14302  hashinfxadd  14310  hashunx  14311  hashunsng  14317  elprchashprn2  14321  hashss  14334  hash1snb  14344  hashmap  14360  hashf1lem2  14381  hashf1  14382  seqcoll  14389  hashle2pr  14402  hashdmpropge2  14408  hashge3el3dif  14412  hash1to3  14417  fundmge2nop0  14427  fi1uzind  14432  brfi1indALT  14435  sswrd  14447  swrdnd2  14580  swrdnnn0nd  14581  swrdnd0  14582  swrdwrdsymb  14587  pfxnd0  14613  swrdswrdlem  14628  swrdswrd  14629  wrd2ind  14647  swrdccatin1  14649  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccat3  14658  repsdf2  14702  repswswrd  14708  cshw0  14718  cshwcl  14722  cshwlen  14723  cshf1  14734  swrdco  14762  relexpsucnnl  14955  rtrclreclem3  14985  rtrclreclem4  14986  relexpindlem  14988  rtrclind  14990  shftlem  14993  caubnd  15284  reusq0  15390  rlimcld2  15503  o1dif  15555  climub  15587  climserle  15588  iseraltlem2  15608  sumss  15649  fsumzcl2  15664  fsummsnunz  15679  fsumsplitsnun  15680  fsum2d  15696  modfsummods  15718  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  climcndslem1  15774  climcndslem2  15775  cvgrat  15808  clim2prod  15813  prodfn0  15819  prodfrec  15820  ntrivcvg  15822  prodmo  15861  fprodss  15873  fprodabs  15899  fprodn0  15904  fprod2d  15906  fprodefsum  16020  ruclem8  16164  ruclem9  16165  dvdsmod0  16187  dvds2ln  16218  dvdsaddre2b  16236  dvdslelem  16238  dvdsdivcl  16245  alzdvds  16249  mod2eq1n2dvds  16276  oddnn02np1  16277  nn0o1gt2  16310  nno  16311  sumeven  16316  sumodd  16317  pwp1fsum  16320  ndvdsadd  16339  bitsinv1  16371  sadcadd  16387  sadadd2  16389  saddisjlem  16393  smuval2  16411  smupvallem  16412  smu01lem  16414  smupval  16417  smueqlem  16419  smumullem  16421  gcddiv  16480  rplpwr  16487  nn0seqcvgd  16499  seq1st  16500  alginv  16504  algcvga  16508  algfx  16509  absprodnn  16547  isprm2  16611  isprm3  16612  prmind2  16614  maxprmfct  16638  prmdvdsexp  16644  pcmpt  16822  prmreclem4  16849  vdwmc2  16909  vdwlem10  16920  ramub2  16944  ramcl  16959  prmgaplem5  16985  prmgaplem8  16988  cshwshashlem1  17025  cshwshashlem3  17027  setsn0fun  17102  imasleval  17463  divsfval  17469  mreexexlem4d  17571  isssc  17745  initoeu1  17936  termoeu1  17943  istos  18340  mgmcl  18535  sgrpidmnd  18631  frmdgsum  18754  smndex1mgm  18799  dfgrp3lem  18935  mhmmulg  19012  resghm2b  19131  gsumwrev  19263  elsymgbas  19271  symgextf1  19318  gsmsymgreqlem2  19328  gsmsymgreq  19329  odlem1  19432  odcl2  19462  gexlem1  19476  efgi2  19622  efginvrel2  19624  efgsrel  19631  cyggexb  19796  gsummulglem  19838  gsumzunsnd  19853  gsum2dlem2  19868  telgsums  19890  dmdprd  19897  dprdw  19909  ablfac1eulem  19971  srgpcomp  20121  rnghmmul  20352  nrhmzr  20440  lmodfopnelem1  20819  rmodislmodlem  20850  cnfldmulg  21328  cnfldexp  21329  nzerooringczr  21405  obslbs  21655  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  cply1mul  22199  coe1fzgsumdlem  22206  gsummoncoe1  22211  pf1ind  22258  evl1gsumdlem  22259  mat1dimcrng  22380  ma1repveval  22474  mulmarep1gsum2  22477  gsummatr01lem3  22560  cramerlem3  22592  decpmatmulsumfsupp  22676  mp2pm2mplem4  22712  pm2mpmhmlem1  22721  fvmptnn04if  22752  cayhamlem1  22769  fctop  22907  mretopd  22995  restopnb  23078  restdis  23081  tgcnp  23156  cncls2  23176  cncls  23177  cnntr  23178  cnsscnp  23182  cmpsub  23303  2ndcsep  23362  1stcelcls  23364  lfinpfin  23427  locfincmp  23429  comppfsc  23435  txcn  23529  txlm  23551  xkohaus  23556  qtopres  23601  haushmphlem  23690  cmphmph  23691  connhmph  23692  reghmph  23696  nrmhmph  23697  ptcmpfi  23716  reghaus  23728  fbssfi  23740  fbun  23743  fbfinnfr  23744  isfildlem  23760  fgcl  23781  cfinfil  23796  supfil  23798  ufinffr  23832  fin1aufil  23835  cnpflf  23904  alexsubALTlem3  23952  alexsubALT  23954  cnextfvval  23968  cnextcn  23970  tmdgsum  23998  tgphaus  24020  tgpt1  24021  mettri  24256  blssexps  24330  blssex  24331  mopni3  24398  metss  24412  psmetutop  24471  dscmet  24476  tngngp3  24560  rectbntr0  24737  metnrmlem1a  24763  fsumcn  24777  lmmbr  25174  caubl  25224  caublcls  25225  bcthlem5  25244  bcth3  25247  ovolunlem1a  25413  ovoliunnul  25424  finiunmbl  25461  voliunlem1  25467  volsuplem  25472  volsup  25473  dyadmax  25515  itgfsum  25744  dvnadd  25847  cpnord  25853  dvnfre  25872  dvmptfsum  25895  dvlip  25914  fta1g  26091  plyco  26162  dgrcolem1  26195  dgrco  26197  dvnply2  26211  plydivex  26221  plyexmo  26237  aannenlem1  26252  aaliou3lem2  26267  dvntaylp  26295  taylthlem1  26297  ulmval  26305  cxpmul2  26614  cxpsqrtth  26655  scvxcvx  26912  jensenlem2  26914  jensen  26915  ppiub  27131  bcmono  27204  bpos1lem  27209  bposlem5  27215  gausslemma2dlem6  27299  lgsquad2lem2  27312  2lgslem3  27331  2lgs  27334  2sqnn  27366  addsqnreup  27370  2sqreultblem  27375  2sqreunnltblem  27378  dchrisumlem1  27416  dchrisum0flb  27437  pntpbnd1  27513  pntlemf  27532  qabvle  27552  qabvexp  27553  ostthlem2  27555  ostth2lem2  27561  sltval2  27584  sltsolem1  27603  negsprop  27964  mulsuniflem  28075  precsexlem6  28137  precsexlem7  28138  noseqind  28209  om2noseqlt  28216  n0addscl  28259  n0mulscl  28260  expsne0  28346  axeuclidlem  28925  axcontlem12  28938  umgrnloopv  29069  uhgredgrnv  29093  edglnl  29106  numedglnl  29107  usgruspgrb  29146  usgrnloopvALT  29164  usgredg2vlem2  29189  subupgr  29250  nbumgr  29310  uhgrnbgr0nb  29317  nbgr0edglem  29319  edgusgrnbfin  29336  nb3grprlem2  29344  uvtxnbgrvtx  29356  cplgrop  29400  cusgrfi  29422  fusgrmaxsize  29428  fusgrn0degnn0  29463  ewlkprop  29567  uspgr2wlkeq  29609  g0wlk0  29614  wlkreslem  29631  lfgriswlk  29650  upgrwlkdvde  29700  spthonepeq  29715  uhgrwkspth  29718  usgr2trlncl  29723  usgr2trlspth  29724  cyclnumvtx  29763  cyclnspth  29764  crctcshwlkn0lem3  29775  wwlksn  29800  wspthneq1eq2  29823  wwlksm1edg  29844  wwlksnred  29855  wwlksnextfun  29861  wwlksnextinj  29862  wwlksnextproplem3  29874  wspthsnonn0vne  29880  wspn0  29887  rusgrnumwwlk  29938  clwwlkccatlem  29951  umgrclwwlkge2  29953  clwlkclwwlklem2  29962  clwlkclwwlklem3  29963  clwwisshclwws  29977  clwwisshclwwsn  29978  clwwlkn1loopb  30005  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  clwwlknonex2lem2  30070  upgr3v3e3cycl  30142  uhgr3cyclex  30144  upgr4cycl4dv4e  30147  eupth2lem3lem4  30193  eupth2lem3lem7  30196  eupth2  30201  eulerpath  30203  nfrgr2v  30234  frgr3vlem1  30235  3vfriswmgr  30240  1to2vfriswmgr  30241  1to3vfriswmgr  30242  3cyclfrgrrn1  30247  3cyclfrgrrn  30248  3cyclfrgrrn2  30249  4cycl2vnunb  30252  frgrncvvdeqlem2  30262  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  frgrwopreglem4a  30272  frgrwopreglem5lem  30282  frgrwopreglem5ALT  30284  frgrregorufr0  30286  frgr2wwlk1  30291  frgr2wwlkeqm  30293  fusgr2wsp2nb  30296  2wspmdisj  30299  frrusgrord  30303  numclwwlk1lem2f1  30319  numclwlk1  30333  frgrreggt1  30355  friendshipgt3  30360  hlim2  31154  elnlfn  31890  stle0i  32201  hstrbi  32228  spansncv2  32255  h1da  32311  fmptcof2  32614  sgn3da  32792  xreceu  32875  domnprodn0  33225  1arithufdlem3  33493  1arithufdlem4  33494  tpr2rico  33878  hasheuni  34051  ismeas  34165  sseqp1  34362  rrvsum  34421  dstfrvunirn  34442  signstfvc  34541  bnj607  34882  bnj1145  34959  bnj1204  34978  fineqvrep  35069  onvf1odlem4  35078  fisshasheq  35087  subgrwlk  35104  subfacp1lem6  35157  cvmlift2lem12  35286  cvmlift3lem4  35294  satfrnmapom  35342  sat1el2xp  35351  satffunlem2  35380  satffun  35381  mrsubvrs  35494  climuzcnv  35643  iprodefisumlem  35712  dfon2lem9  35764  linethru  36126  elhf2  36148  finminlem  36291  fnessref  36330  neibastop2lem  36333  fnemeet2  36340  nndivsub  36430  bj-xpnzex  36932  bj-elpwg  37025  bj-epelg  37041  mptsnunlem  37311  dissneqlem  37313  topdifinffinlem  37320  iooelexlt  37335  domalom  37377  fvineqsneq  37385  wl-exeq  37507  wl-ax11-lem3  37560  matunitlindflem1  37595  poimirlem22  37621  poimirlem26  37625  poimirlem28  37627  poimirlem29  37628  poimirlem32  37631  heicant  37634  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  cover2  37694  upixp  37708  sdclem2  37721  fdc  37724  seqpo  37726  metf1o  37734  mettrifi  37736  sstotbnd3  37755  heibor1lem  37788  heiborlem5  37794  heibor  37800  bfplem1  37801  elghomlem2OLD  37865  grpokerinj  37872  isrngo  37876  rngodm1dm2  37911  ispridl2  38017  exlimddvf  38100  lssatle  38993  4atexlemex4  40052  uzindd  41950  evl1gprodd  42090  sn-axprlem3  42190  redvmptabs  42333  sn-sup3d  42465  mzpsubst  42721  jm2.18  42961  wepwsolem  43015  oaabsb  43267  oacl2g  43303  ofoafg  43327  ofoaid1  43331  ofoaid2  43332  naddonnn  43368  iunrelexp0  43675  relexpmulg  43683  cnvtrclfv  43697  clsk1indlem3  44016  grucollcld  44233  inaex  44270  dvgrat  44285  radcnvrat  44287  csbxpgVD  44867  sineq0ALT  44910  trfr  44936  relwf  44941  pwclaxpow  44958  omssaxinf2  44962  islptre  45601  iblspltprt  45955  stoweidlem2  45984  stoweidlem17  45999  stoweidlem21  46003  2reuimp0  47099  2reuimp  47100  afveu  47138  funbrafv  47143  ndmaovass  47191  afv2eu  47223  tz6.12c-afv2  47227  funop1  47268  f1oresf1o2  47276  fvmptrabdm  47278  nltle2tri  47298  2elfz2melfz  47303  fsummsndifre  47357  fsumsplitsndif  47358  fsummmodsndifre  47359  fsummmodsnunz  47360  elsetpreimafvssdm  47371  uniimaelsetpreimafv  47381  imasetpreimafvbijlemfv1  47388  iccpartiltu  47407  iccpartigtl  47408  iccpartleu  47413  iccpartgel  47414  iccpartrn  47415  iccpartiun  47419  icceuelpart  47421  iccpartnel  47423  fargshiftf  47425  fargshiftf1  47426  ichnfb  47450  elsprel  47460  prsprel  47472  sprsymrelfo  47482  paireqne  47496  sbcpr  47506  reupr  47507  fmtnoinf  47521  odz2prm2pw  47548  lighneallem4  47595  lighneal  47596  requad1  47607  requad2  47608  evensumeven  47692  even3prm2  47704  gbowgt5  47747  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  bgoldbnnsum3prm  47789  bgoldbtbndlem2  47791  bgoldbtbndlem4  47793  bgoldbtbnd  47794  dfsclnbgr6  47843  grimco  47874  cycl3grtri  47932  isubgr3stgrlem6  47956  gricgrlic  48003  gpgedgvtx0  48046  gpgprismgr4cycllem3  48082  pgnbgreunbgrlem5  48108  clcllaw  48176  rngccatidALTV  48257  ringccatidALTV  48291  scmsuppss  48356  gsumlsscl  48365  ply1mulgsumlem2  48373  lincvalsc0  48407  linc0scn0  48409  lincdifsn  48410  linc1  48411  lincellss  48412  lincsum  48415  lincscm  48416  lincsumcl  48417  lcoss  48422  lincext3  48442  lindslinindimp2lem4  48447  lindslinindsimp2lem5  48448  lindslinindsimp2  48449  lindsrng01  48454  snlindsntor  48457  lincresunit3lem2  48466  lincresunit3  48467  islindeps2  48469  blengt1fldiv2p1  48579  2arymaptf1  48639  resum2sqorgt0  48695  reorelicc  48696  rrx2plordisom  48709  rrx2linest  48728  rrxsphere  48734  line2ylem  48737  itsclc0xyqsol  48754  itscnhlinecirc02p  48771  mo0sn  48801  thincn0eu  49417