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  3230  cbvraldva2  3321  rspcebdv  3582  2reu2  3861  csbie2df  4406  minel  4429  uneqdifeq  4456  raltpd  4745  ssunsn2  4791  opthprneg  4829  ssuni  4896  uniss2  4905  elpwuni  5069  intss2  5072  disjord  5096  elpw2g  5288  elssabg  5298  axprlem3OLD  5383  axprlem4OLD  5384  axprlem5OLD  5385  oteqex  5460  otsndisj  5479  otiunsndisj  5480  epelg  5539  wereu  5634  relop  5814  riinint  5935  sotri3  6103  unixpid  6257  reuop  6266  ordtr2  6377  ordsssuc2  6425  iotan0  6501  funopg  6550  fun  6722  tz6.12cOLD  6885  fvmptnf  6990  fvn0ssdmfun  7046  eldmrexrnb  7064  fmptco  7101  fnressn  7130  fressnfv  7132  fprb  7168  fvtp2g  7173  fvtp3g  7174  fconst2g  7177  fntpb  7183  f1dom3el3dif  7244  f1ounsn  7247  isores3  7310  isoselem  7316  oprabv  7449  eloprabga  7498  sorpsscmpl  7710  difex2  7736  ordpwsuc  7790  ordsucun  7800  limuni3  7828  trom  7851  fo1stres  7994  poxp  8107  soxp  8108  xpord3inddlem  8133  soseq  8138  suppimacnv  8153  fsuppeq  8154  funsssuppss  8169  brtpos2  8211  frrlem8  8272  fpr2a  8281  onnseq  8313  smores  8321  smofvon2  8325  tfrlem1  8344  oacl  8499  omcl  8500  oecl  8501  oawordri  8514  oalimcl  8524  oaass  8525  oarec  8526  omwordri  8536  omeulem1  8546  omeulem2  8547  oeordi  8551  oeworde  8557  oeoelem  8562  nnacl  8575  nnmcl  8576  nnecl  8577  nnacom  8581  nnaass  8586  nnmsucr  8589  nnmordi  8595  omabs  8615  cofonr  8638  naddunif  8657  iiner  8762  elpmg  8816  fsetfcdm  8833  fsetprcnex  8835  pmss12g  8842  mapfvd  8852  f1domg  8943  ssdomg  8971  undom  9029  domtriord  9087  ssnnfi  9133  fnfi  9142  enfi  9151  php  9171  sdom1  9189  1sdom2dom  9194  1sdomOLD  9196  fisseneq  9204  isinf  9207  isinfOLD  9208  dif1ennnALT  9222  findcard3  9229  findcard3OLD  9230  frfi  9232  difinf  9260  imafiOLD  9265  iunfi  9294  fsuppunfi  9339  fsuppres  9344  ffsuppbi  9349  elfi2  9365  marypha1lem  9384  marypha1  9385  oiexg  9488  wemapso2  9506  harword  9516  brwdom  9520  unxpwdom  9542  en3lplem1  9565  inf3lemd  9580  inf3lem5  9585  cantnfval2  9622  cantnfle  9624  cantnflt  9625  cnfcom  9653  tcmin  9694  frr2  9713  r1sdom  9727  rankxplim3  9834  cardidm  9912  cardmin2  9952  infxpenlem  9966  fseqenlem1  9977  numacn  10002  alephordi  10027  iscard3  10046  alephinit  10048  carduniima  10049  iunfictbso  10067  dfac5  10082  dfac12lem3  10099  nnadju  10151  pwsdompw  10156  pwdjudom  10168  cflim2  10216  cfslb2n  10221  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  alephsing  10229  infpssALT  10266  fin23lem34  10299  isf32lem2  10307  isf32lem10  10315  isf32lem12  10317  isfin1-2  10338  hsmexlem4  10382  axcc2lem  10389  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  ac6num  10432  ac6s  10437  zorn2lem7  10455  ttukeylem5  10466  imadomg  10487  iundom2g  10493  ondomon  10516  ficard  10518  konigthlem  10521  alephreg  10535  pwcfsdom  10536  cfpwsdom  10537  axregndlem1  10555  axregnd  10557  pwfseqlem3  10613  pwxpndom2  10618  pwxpndom  10619  pwdjundom  10620  inawinalem  10642  gchina  10652  wuncval2  10700  tsk0  10716  tskxpss  10725  inatsk  10731  tskuni  10736  gruina  10771  grothac  10783  addclpi  10845  addnidpi  10854  nqereu  10882  mulcanenq  10913  genpnnp  10958  nqpr  10967  prlem934  10986  reclem2pr  11001  suplem1pr  11005  supsrlem  11064  axpre-sup  11122  1re  11174  dedekindle  11338  00id  11349  receu  11823  sup3  12140  infrelb  12168  peano5nni  12189  nnindd  12206  nnaddcl  12209  zrevaddcl  12578  nzadd  12581  zdiv  12604  nneo  12618  zeo2  12621  nn0indd  12631  fzind  12632  fnn0ind  12633  fzindd  12636  uzwo  12870  lbzbi  12895  nn01to3  12900  qrevaddcl  12930  irradd  12932  irrmul  12933  ltsubrp  12989  ltaddrp  12990  xnn0xaddcl  13195  xnn0xadd0  13207  icoshft  13434  fzen  13502  elfzm11  13556  uzsplit  13557  elfzom1elp1fzo  13693  fzoopth  13723  injresinjlem  13748  injresinj  13749  modifeq2int  13898  modsumfzodifsn  13909  om2uzlti  13915  ssnn0fi  13950  fsuppmapnn0fiub0  13958  mptnn0fsuppr  13964  seqcaopr3  14002  seqf1olem2a  14005  seqf1o  14008  ser1const  14023  expadd  14069  expmul  14072  leexp1a  14140  faccl  14248  facdiv  14252  faclbnd  14255  faclbnd4lem4  14261  hasheqf1oi  14316  hashgadd  14342  hashinfxadd  14350  hashunx  14351  hashunsng  14357  elprchashprn2  14361  hashss  14374  hash1snb  14384  hashmap  14400  hashf1lem2  14421  hashf1  14422  seqcoll  14429  hashle2pr  14442  hashdmpropge2  14448  hashge3el3dif  14452  hash1to3  14457  fundmge2nop0  14467  fi1uzind  14472  brfi1indALT  14475  sswrd  14487  swrdnd2  14620  swrdnnn0nd  14621  swrdnd0  14622  swrdwrdsymb  14627  pfxnd0  14653  swrdswrdlem  14669  swrdswrd  14670  wrd2ind  14688  swrdccatin1  14690  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccat3  14699  repsdf2  14743  repswswrd  14749  cshw0  14759  cshwcl  14763  cshwlen  14764  cshf1  14775  swrdco  14803  relexpsucnnl  14996  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  rtrclind  15031  shftlem  15034  caubnd  15325  reusq0  15431  rlimcld2  15544  o1dif  15596  climub  15628  climserle  15629  iseraltlem2  15649  sumss  15690  fsumzcl2  15705  fsummsnunz  15720  fsumsplitsnun  15721  fsum2d  15737  modfsummods  15759  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  climcndslem1  15815  climcndslem2  15816  cvgrat  15849  clim2prod  15854  prodfn0  15860  prodfrec  15861  ntrivcvg  15863  prodmo  15902  fprodss  15914  fprodabs  15940  fprodn0  15945  fprod2d  15947  fprodefsum  16061  ruclem8  16205  ruclem9  16206  dvdsmod0  16228  dvds2ln  16259  dvdsaddre2b  16277  dvdslelem  16279  dvdsdivcl  16286  alzdvds  16290  mod2eq1n2dvds  16317  oddnn02np1  16318  nn0o1gt2  16351  nno  16352  sumeven  16357  sumodd  16358  pwp1fsum  16361  ndvdsadd  16380  bitsinv1  16412  sadcadd  16428  sadadd2  16430  saddisjlem  16434  smuval2  16452  smupvallem  16453  smu01lem  16455  smupval  16458  smueqlem  16460  smumullem  16462  gcddiv  16521  rplpwr  16528  nn0seqcvgd  16540  seq1st  16541  alginv  16545  algcvga  16549  algfx  16550  absprodnn  16588  isprm2  16652  isprm3  16653  prmind2  16655  maxprmfct  16679  prmdvdsexp  16685  pcmpt  16863  prmreclem4  16890  vdwmc2  16950  vdwlem10  16961  ramub2  16985  ramcl  17000  prmgaplem5  17026  prmgaplem8  17029  cshwshashlem1  17066  cshwshashlem3  17068  setsn0fun  17143  imasleval  17504  divsfval  17510  mreexexlem4d  17608  isssc  17782  initoeu1  17973  termoeu1  17980  istos  18377  mgmcl  18570  sgrpidmnd  18666  frmdgsum  18789  smndex1mgm  18834  dfgrp3lem  18970  mhmmulg  19047  resghm2b  19166  gsumwrev  19298  elsymgbas  19304  symgextf1  19351  gsmsymgreqlem2  19361  gsmsymgreq  19362  odlem1  19465  odcl2  19495  gexlem1  19509  efgi2  19655  efginvrel2  19657  efgsrel  19664  cyggexb  19829  gsummulglem  19871  gsumzunsnd  19886  gsum2dlem2  19901  telgsums  19923  dmdprd  19930  dprdw  19942  ablfac1eulem  20004  srgpcomp  20127  rnghmmul  20358  nrhmzr  20446  lmodfopnelem1  20804  rmodislmodlem  20835  cnfldmulg  21315  cnfldexp  21316  nzerooringczr  21390  obslbs  21639  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  cply1mul  22183  coe1fzgsumdlem  22190  gsummoncoe1  22195  pf1ind  22242  evl1gsumdlem  22243  mat1dimcrng  22364  ma1repveval  22458  mulmarep1gsum2  22461  gsummatr01lem3  22544  cramerlem3  22576  decpmatmulsumfsupp  22660  mp2pm2mplem4  22696  pm2mpmhmlem1  22705  fvmptnn04if  22736  cayhamlem1  22753  fctop  22891  mretopd  22979  restopnb  23062  restdis  23065  tgcnp  23140  cncls2  23160  cncls  23161  cnntr  23162  cnsscnp  23166  cmpsub  23287  2ndcsep  23346  1stcelcls  23348  lfinpfin  23411  locfincmp  23413  comppfsc  23419  txcn  23513  txlm  23535  xkohaus  23540  qtopres  23585  haushmphlem  23674  cmphmph  23675  connhmph  23676  reghmph  23680  nrmhmph  23681  ptcmpfi  23700  reghaus  23712  fbssfi  23724  fbun  23727  fbfinnfr  23728  isfildlem  23744  fgcl  23765  cfinfil  23780  supfil  23782  ufinffr  23816  fin1aufil  23819  cnpflf  23888  alexsubALTlem3  23936  alexsubALT  23938  cnextfvval  23952  cnextcn  23954  tmdgsum  23982  tgphaus  24004  tgpt1  24005  mettri  24240  blssexps  24314  blssex  24315  mopni3  24382  metss  24396  psmetutop  24455  dscmet  24460  tngngp3  24544  rectbntr0  24721  metnrmlem1a  24747  fsumcn  24761  lmmbr  25158  caubl  25208  caublcls  25209  bcthlem5  25228  bcth3  25231  ovolunlem1a  25397  ovoliunnul  25408  finiunmbl  25445  voliunlem1  25451  volsuplem  25456  volsup  25457  dyadmax  25499  itgfsum  25728  dvnadd  25831  cpnord  25837  dvnfre  25856  dvmptfsum  25879  dvlip  25898  fta1g  26075  plyco  26146  dgrcolem1  26179  dgrco  26181  dvnply2  26195  plydivex  26205  plyexmo  26221  aannenlem1  26236  aaliou3lem2  26251  dvntaylp  26279  taylthlem1  26281  ulmval  26289  cxpmul2  26598  cxpsqrtth  26639  scvxcvx  26896  jensenlem2  26898  jensen  26899  ppiub  27115  bcmono  27188  bpos1lem  27193  bposlem5  27199  gausslemma2dlem6  27283  lgsquad2lem2  27296  2lgslem3  27315  2lgs  27318  2sqnn  27350  addsqnreup  27354  2sqreultblem  27359  2sqreunnltblem  27362  dchrisumlem1  27400  dchrisum0flb  27421  pntpbnd1  27497  pntlemf  27516  qabvle  27536  qabvexp  27537  ostthlem2  27539  ostth2lem2  27545  sltval2  27568  sltsolem1  27587  negsprop  27941  mulsuniflem  28052  precsexlem6  28114  precsexlem7  28115  noseqind  28186  om2noseqlt  28193  n0addscl  28236  n0mulscl  28237  expsne0  28321  axeuclidlem  28889  axcontlem12  28902  umgrnloopv  29033  uhgredgrnv  29057  edglnl  29070  numedglnl  29071  usgruspgrb  29110  usgrnloopvALT  29128  usgredg2vlem2  29153  subupgr  29214  nbumgr  29274  uhgrnbgr0nb  29281  nbgr0edglem  29283  edgusgrnbfin  29300  nb3grprlem2  29308  uvtxnbgrvtx  29320  cplgrop  29364  cusgrfi  29386  fusgrmaxsize  29392  fusgrn0degnn0  29427  ewlkprop  29531  uspgr2wlkeq  29574  g0wlk0  29580  wlkreslem  29597  lfgriswlk  29616  upgrwlkdvde  29667  spthonepeq  29682  uhgrwkspth  29685  usgr2trlncl  29690  usgr2trlspth  29691  cyclnumvtx  29730  cyclnspth  29731  crctcshwlkn0lem3  29742  wwlksn  29767  wspthneq1eq2  29790  wwlksm1edg  29811  wwlksnred  29822  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextproplem3  29841  wspthsnonn0vne  29847  wspn0  29854  rusgrnumwwlk  29905  clwwlkccatlem  29918  umgrclwwlkge2  29920  clwlkclwwlklem2  29929  clwlkclwwlklem3  29930  clwwisshclwws  29944  clwwisshclwwsn  29945  clwwlkn1loopb  29972  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwlknonex2lem2  30037  upgr3v3e3cycl  30109  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  eupth2lem3lem4  30160  eupth2lem3lem7  30163  eupth2  30168  eulerpath  30170  nfrgr2v  30201  frgr3vlem1  30202  3vfriswmgr  30207  1to2vfriswmgr  30208  1to3vfriswmgr  30209  3cyclfrgrrn1  30214  3cyclfrgrrn  30215  3cyclfrgrrn2  30216  4cycl2vnunb  30219  frgrncvvdeqlem2  30229  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  frgrwopreglem4a  30239  frgrwopreglem5lem  30249  frgrwopreglem5ALT  30251  frgrregorufr0  30253  frgr2wwlk1  30258  frgr2wwlkeqm  30260  fusgr2wsp2nb  30263  2wspmdisj  30266  frrusgrord  30270  numclwwlk1lem2f1  30286  numclwlk1  30300  frgrreggt1  30322  friendshipgt3  30327  hlim2  31121  elnlfn  31857  stle0i  32168  hstrbi  32195  spansncv2  32222  h1da  32278  fmptcof2  32581  sgn3da  32759  xreceu  32842  domnprodn0  33226  1arithufdlem3  33517  1arithufdlem4  33518  tpr2rico  33902  hasheuni  34075  ismeas  34189  sseqp1  34386  rrvsum  34445  dstfrvunirn  34466  signstfvc  34565  bnj607  34906  bnj1145  34983  bnj1204  35002  fineqvrep  35085  onvf1odlem4  35093  fisshasheq  35102  subgrwlk  35119  subfacp1lem6  35172  cvmlift2lem12  35301  cvmlift3lem4  35309  satfrnmapom  35357  sat1el2xp  35366  satffunlem2  35395  satffun  35396  mrsubvrs  35509  climuzcnv  35658  iprodefisumlem  35727  dfon2lem9  35779  linethru  36141  elhf2  36163  finminlem  36306  fnessref  36345  neibastop2lem  36348  fnemeet2  36355  nndivsub  36445  bj-xpnzex  36947  bj-elpwg  37040  bj-epelg  37056  mptsnunlem  37326  dissneqlem  37328  topdifinffinlem  37335  iooelexlt  37350  domalom  37392  fvineqsneq  37400  wl-exeq  37522  wl-ax11-lem3  37575  matunitlindflem1  37610  poimirlem22  37636  poimirlem26  37640  poimirlem28  37642  poimirlem29  37643  poimirlem32  37646  heicant  37649  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  cover2  37709  upixp  37723  sdclem2  37736  fdc  37739  seqpo  37741  metf1o  37749  mettrifi  37751  sstotbnd3  37770  heibor1lem  37803  heiborlem5  37809  heibor  37815  bfplem1  37816  elghomlem2OLD  37880  grpokerinj  37887  isrngo  37891  rngodm1dm2  37926  ispridl2  38032  exlimddvf  38115  lssatle  39008  4atexlemex4  40067  uzindd  41965  evl1gprodd  42105  sn-axprlem3  42205  redvmptabs  42348  sn-sup3d  42480  mzpsubst  42736  jm2.18  42977  wepwsolem  43031  oaabsb  43283  oacl2g  43319  ofoafg  43343  ofoaid1  43347  ofoaid2  43348  naddonnn  43384  iunrelexp0  43691  relexpmulg  43699  cnvtrclfv  43713  clsk1indlem3  44032  grucollcld  44249  inaex  44286  dvgrat  44301  radcnvrat  44303  csbxpgVD  44883  sineq0ALT  44926  trfr  44952  relwf  44957  pwclaxpow  44974  omssaxinf2  44978  islptre  45617  iblspltprt  45971  stoweidlem2  46000  stoweidlem17  46015  stoweidlem21  46019  2reuimp0  47115  2reuimp  47116  afveu  47154  funbrafv  47159  ndmaovass  47207  afv2eu  47239  tz6.12c-afv2  47243  funop1  47284  f1oresf1o2  47292  fvmptrabdm  47294  nltle2tri  47314  2elfz2melfz  47319  fsummsndifre  47373  fsumsplitsndif  47374  fsummmodsndifre  47375  fsummmodsnunz  47376  elsetpreimafvssdm  47387  uniimaelsetpreimafv  47397  imasetpreimafvbijlemfv1  47404  iccpartiltu  47423  iccpartigtl  47424  iccpartleu  47429  iccpartgel  47430  iccpartrn  47431  iccpartiun  47435  icceuelpart  47437  iccpartnel  47439  fargshiftf  47441  fargshiftf1  47442  ichnfb  47466  elsprel  47476  prsprel  47488  sprsymrelfo  47498  paireqne  47512  sbcpr  47522  reupr  47523  fmtnoinf  47537  odz2prm2pw  47564  lighneallem4  47611  lighneal  47612  requad1  47623  requad2  47624  evensumeven  47708  even3prm2  47720  gbowgt5  47763  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem4  47809  bgoldbtbnd  47810  dfsclnbgr6  47858  grimco  47889  cycl3grtri  47946  isubgr3stgrlem6  47970  gricgrlic  48010  gpgedgvtx0  48052  gpgprismgr4cycllem3  48087  pgnbgreunbgrlem5  48113  clcllaw  48179  rngccatidALTV  48260  ringccatidALTV  48294  scmsuppss  48359  gsumlsscl  48368  ply1mulgsumlem2  48376  lincvalsc0  48410  linc0scn0  48412  lincdifsn  48413  linc1  48414  lincellss  48415  lincsum  48418  lincscm  48419  lincsumcl  48420  lcoss  48425  lincext3  48445  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lindsrng01  48457  snlindsntor  48460  lincresunit3lem2  48469  lincresunit3  48470  islindeps2  48472  blengt1fldiv2p1  48582  2arymaptf1  48642  resum2sqorgt0  48698  reorelicc  48699  rrx2plordisom  48712  rrx2linest  48731  rrxsphere  48737  line2ylem  48740  itsclc0xyqsol  48757  itscnhlinecirc02p  48774  mo0sn  48804  thincn0eu  49420