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  2098  mo4  2561  2moswapv  2624  2moswap  2639  2mosOLD  2645  2eu2  2648  pm2.61ne  3013  nelelne  3027  r19.21be  3225  cbvraldva2  3314  rspcebdv  3571  2reu2  3849  csbie2df  4393  minel  4416  uneqdifeq  4443  raltpd  4734  ssunsn2  4779  opthprneg  4817  ssuni  4884  uniss2  4892  elpwuni  5053  intss2  5056  disjord  5080  elpw2g  5271  elssabg  5281  axprlem3OLD  5366  axprlem4OLD  5367  axprlem5OLD  5368  oteqex  5440  otsndisj  5459  otiunsndisj  5460  epelg  5517  wereu  5612  relop  5790  riinint  5911  sotri3  6077  unixpid  6231  reuop  6240  ordtr2  6351  ordsssuc2  6399  iotan0  6471  funopg  6515  fun  6685  fvmptnf  6951  fvn0ssdmfun  7007  eldmrexrnb  7025  fmptco  7062  fnressn  7091  fressnfv  7093  fprb  7128  fvtp2g  7133  fvtp3g  7134  fconst2g  7137  fntpb  7143  f1dom3el3dif  7203  f1ounsn  7206  isores3  7269  isoselem  7275  oprabv  7406  eloprabga  7455  sorpsscmpl  7667  difex2  7693  ordpwsuc  7745  ordsucun  7755  limuni3  7782  trom  7805  fo1stres  7947  poxp  8058  soxp  8059  xpord3inddlem  8084  soseq  8089  suppimacnv  8104  fsuppeq  8105  funsssuppss  8120  brtpos2  8162  frrlem8  8223  fpr2a  8232  onnseq  8264  smores  8272  smofvon2  8276  tfrlem1  8295  oacl  8450  omcl  8451  oecl  8452  oawordri  8465  oalimcl  8475  oaass  8476  oarec  8477  omwordri  8487  omeulem1  8497  omeulem2  8498  oeordi  8502  oeworde  8508  oeoelem  8513  nnacl  8526  nnmcl  8527  nnecl  8528  nnacom  8532  nnaass  8537  nnmsucr  8540  nnmordi  8546  omabs  8566  cofonr  8589  naddunif  8608  iiner  8713  elpmg  8767  fsetfcdm  8784  fsetprcnex  8786  pmss12g  8793  mapfvd  8803  f1domg  8894  ssdomg  8922  undom  8978  domtriord  9036  ssnnfi  9079  fnfi  9087  enfi  9096  php  9116  sdom1  9134  1sdom2dom  9138  fisseneq  9147  isinf  9149  dif1ennnALT  9161  findcard3  9167  frfi  9169  difinf  9195  imafiOLD  9200  iunfi  9227  fsuppunfi  9272  fsuppres  9277  ffsuppbi  9282  elfi2  9298  marypha1lem  9317  marypha1  9318  oiexg  9421  wemapso2  9439  harword  9449  brwdom  9453  unxpwdom  9475  en3lplem1  9502  inf3lemd  9517  inf3lem5  9522  cantnfval2  9559  cantnfle  9561  cantnflt  9562  cnfcom  9590  tcmin  9631  frr2  9650  r1sdom  9664  rankxplim3  9771  cardidm  9849  cardmin2  9889  infxpenlem  9901  fseqenlem1  9912  numacn  9937  alephordi  9962  iscard3  9981  alephinit  9983  carduniima  9984  iunfictbso  10002  dfac5  10017  dfac12lem3  10034  nnadju  10086  pwsdompw  10091  pwdjudom  10103  cflim2  10151  cfslb2n  10156  cofsmo  10157  cfsmolem  10158  cfcoflem  10160  alephsing  10164  infpssALT  10201  fin23lem34  10234  isf32lem2  10242  isf32lem10  10250  isf32lem12  10252  isfin1-2  10273  hsmexlem4  10317  axcc2lem  10324  domtriomlem  10330  axdc2lem  10336  axdc3lem2  10339  axdc3lem4  10341  axdc4lem  10343  axcclem  10345  ac6num  10367  ac6s  10372  zorn2lem7  10390  ttukeylem5  10401  imadomg  10422  iundom2g  10428  ondomon  10451  ficard  10453  konigthlem  10456  alephreg  10470  pwcfsdom  10471  cfpwsdom  10472  axregndlem1  10490  axregnd  10492  pwfseqlem3  10548  pwxpndom2  10553  pwxpndom  10554  pwdjundom  10555  inawinalem  10577  gchina  10587  wuncval2  10635  tsk0  10651  tskxpss  10660  inatsk  10666  tskuni  10671  gruina  10706  grothac  10718  addclpi  10780  addnidpi  10789  nqereu  10817  mulcanenq  10848  genpnnp  10893  nqpr  10902  prlem934  10921  reclem2pr  10936  suplem1pr  10940  supsrlem  10999  axpre-sup  11057  1re  11109  dedekindle  11274  00id  11285  receu  11759  sup3  12076  infrelb  12104  peano5nni  12125  nnindd  12142  nnaddcl  12145  zrevaddcl  12514  nzadd  12517  zdiv  12540  nneo  12554  zeo2  12557  nn0indd  12567  fzind  12568  fnn0ind  12569  fzindd  12572  uzwo  12806  lbzbi  12831  nn01to3  12836  qrevaddcl  12866  irradd  12868  irrmul  12869  ltsubrp  12925  ltaddrp  12926  xnn0xaddcl  13131  xnn0xadd0  13143  icoshft  13370  fzen  13438  elfzm11  13492  uzsplit  13493  elfzom1elp1fzo  13629  fzoopth  13659  injresinjlem  13687  injresinj  13688  modifeq2int  13837  modsumfzodifsn  13848  om2uzlti  13854  ssnn0fi  13889  fsuppmapnn0fiub0  13897  mptnn0fsuppr  13903  seqcaopr3  13941  seqf1olem2a  13944  seqf1o  13947  ser1const  13962  expadd  14008  expmul  14011  leexp1a  14079  faccl  14187  facdiv  14191  faclbnd  14194  faclbnd4lem4  14200  hasheqf1oi  14255  hashgadd  14281  hashinfxadd  14289  hashunx  14290  hashunsng  14296  elprchashprn2  14300  hashss  14313  hash1snb  14323  hashmap  14339  hashf1lem2  14360  hashf1  14361  seqcoll  14368  hashle2pr  14381  hashdmpropge2  14387  hashge3el3dif  14391  hash1to3  14396  fundmge2nop0  14406  fi1uzind  14411  brfi1indALT  14414  sswrd  14426  swrdnd2  14560  swrdnnn0nd  14561  swrdnd0  14562  swrdwrdsymb  14567  pfxnd0  14593  swrdswrdlem  14608  swrdswrd  14609  wrd2ind  14627  swrdccatin1  14629  swrdccatin2  14633  pfxccatin12lem2  14635  pfxccat3  14638  repsdf2  14682  repswswrd  14688  cshw0  14698  cshwcl  14702  cshwlen  14703  cshf1  14714  swrdco  14741  relexpsucnnl  14934  rtrclreclem3  14964  rtrclreclem4  14965  relexpindlem  14967  rtrclind  14969  shftlem  14972  caubnd  15263  reusq0  15369  rlimcld2  15482  o1dif  15534  climub  15566  climserle  15567  iseraltlem2  15587  sumss  15628  fsumzcl2  15643  fsummsnunz  15658  fsumsplitsnun  15659  fsum2d  15675  modfsummods  15697  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  climcndslem1  15753  climcndslem2  15754  cvgrat  15787  clim2prod  15792  prodfn0  15798  prodfrec  15799  ntrivcvg  15801  prodmo  15840  fprodss  15852  fprodabs  15878  fprodn0  15883  fprod2d  15885  fprodefsum  15999  ruclem8  16143  ruclem9  16144  dvdsmod0  16166  dvds2ln  16197  dvdsaddre2b  16215  dvdslelem  16217  dvdsdivcl  16224  alzdvds  16228  mod2eq1n2dvds  16255  oddnn02np1  16256  nn0o1gt2  16289  nno  16290  sumeven  16295  sumodd  16296  pwp1fsum  16299  ndvdsadd  16318  bitsinv1  16350  sadcadd  16366  sadadd2  16368  saddisjlem  16372  smuval2  16390  smupvallem  16391  smu01lem  16393  smupval  16396  smueqlem  16398  smumullem  16400  gcddiv  16459  rplpwr  16466  nn0seqcvgd  16478  seq1st  16479  alginv  16483  algcvga  16487  algfx  16488  absprodnn  16526  isprm2  16590  isprm3  16591  prmind2  16593  maxprmfct  16617  prmdvdsexp  16623  pcmpt  16801  prmreclem4  16828  vdwmc2  16888  vdwlem10  16899  ramub2  16923  ramcl  16938  prmgaplem5  16964  prmgaplem8  16967  cshwshashlem1  17004  cshwshashlem3  17006  setsn0fun  17081  imasleval  17442  divsfval  17448  mreexexlem4d  17550  isssc  17724  initoeu1  17915  termoeu1  17922  istos  18319  chnfibg  18539  mgmcl  18548  sgrpidmnd  18644  frmdgsum  18767  smndex1mgm  18812  dfgrp3lem  18948  mhmmulg  19025  resghm2b  19144  gsumwrev  19276  elsymgbas  19284  symgextf1  19331  gsmsymgreqlem2  19341  gsmsymgreq  19342  odlem1  19445  odcl2  19475  gexlem1  19489  efgi2  19635  efginvrel2  19637  efgsrel  19644  cyggexb  19809  gsummulglem  19851  gsumzunsnd  19866  gsum2dlem2  19881  telgsums  19903  dmdprd  19910  dprdw  19922  ablfac1eulem  19984  srgpcomp  20134  rnghmmul  20365  nrhmzr  20450  lmodfopnelem1  20829  rmodislmodlem  20860  cnfldmulg  21338  cnfldexp  21339  nzerooringczr  21415  obslbs  21665  mplcoe1  21970  mplcoe3  21971  mplcoe5  21973  cply1mul  22209  coe1fzgsumdlem  22216  gsummoncoe1  22221  pf1ind  22268  evl1gsumdlem  22269  mat1dimcrng  22390  ma1repveval  22484  mulmarep1gsum2  22487  gsummatr01lem3  22570  cramerlem3  22602  decpmatmulsumfsupp  22686  mp2pm2mplem4  22722  pm2mpmhmlem1  22731  fvmptnn04if  22762  cayhamlem1  22779  fctop  22917  mretopd  23005  restopnb  23088  restdis  23091  tgcnp  23166  cncls2  23186  cncls  23187  cnntr  23188  cnsscnp  23192  cmpsub  23313  2ndcsep  23372  1stcelcls  23374  lfinpfin  23437  locfincmp  23439  comppfsc  23445  txcn  23539  txlm  23561  xkohaus  23566  qtopres  23611  haushmphlem  23700  cmphmph  23701  connhmph  23702  reghmph  23706  nrmhmph  23707  ptcmpfi  23726  reghaus  23738  fbssfi  23750  fbun  23753  fbfinnfr  23754  isfildlem  23770  fgcl  23791  cfinfil  23806  supfil  23808  ufinffr  23842  fin1aufil  23845  cnpflf  23914  alexsubALTlem3  23962  alexsubALT  23964  cnextfvval  23978  cnextcn  23980  tmdgsum  24008  tgphaus  24030  tgpt1  24031  mettri  24265  blssexps  24339  blssex  24340  mopni3  24407  metss  24421  psmetutop  24480  dscmet  24485  tngngp3  24569  rectbntr0  24746  metnrmlem1a  24772  fsumcn  24786  lmmbr  25183  caubl  25233  caublcls  25234  bcthlem5  25253  bcth3  25256  ovolunlem1a  25422  ovoliunnul  25433  finiunmbl  25470  voliunlem1  25476  volsuplem  25481  volsup  25482  dyadmax  25524  itgfsum  25753  dvnadd  25856  cpnord  25862  dvnfre  25881  dvmptfsum  25904  dvlip  25923  fta1g  26100  plyco  26171  dgrcolem1  26204  dgrco  26206  dvnply2  26220  plydivex  26230  plyexmo  26246  aannenlem1  26261  aaliou3lem2  26276  dvntaylp  26304  taylthlem1  26306  ulmval  26314  cxpmul2  26623  cxpsqrtth  26664  scvxcvx  26921  jensenlem2  26923  jensen  26924  ppiub  27140  bcmono  27213  bpos1lem  27218  bposlem5  27224  gausslemma2dlem6  27308  lgsquad2lem2  27321  2lgslem3  27340  2lgs  27343  2sqnn  27375  addsqnreup  27379  2sqreultblem  27384  2sqreunnltblem  27387  dchrisumlem1  27425  dchrisum0flb  27446  pntpbnd1  27522  pntlemf  27541  qabvle  27561  qabvexp  27562  ostthlem2  27564  ostth2lem2  27570  sltval2  27593  sltsolem1  27612  negsprop  27975  mulsuniflem  28086  precsexlem6  28148  precsexlem7  28149  noseqind  28220  om2noseqlt  28227  n0addscl  28270  n0mulscl  28271  expsne0  28357  axeuclidlem  28938  axcontlem12  28951  umgrnloopv  29082  uhgredgrnv  29106  edglnl  29119  numedglnl  29120  usgruspgrb  29159  usgrnloopvALT  29177  usgredg2vlem2  29202  subupgr  29263  nbumgr  29323  uhgrnbgr0nb  29330  nbgr0edglem  29332  edgusgrnbfin  29349  nb3grprlem2  29357  uvtxnbgrvtx  29369  cplgrop  29413  cusgrfi  29435  fusgrmaxsize  29441  fusgrn0degnn0  29476  ewlkprop  29580  uspgr2wlkeq  29622  g0wlk0  29627  wlkreslem  29644  lfgriswlk  29663  upgrwlkdvde  29713  spthonepeq  29728  uhgrwkspth  29731  usgr2trlncl  29736  usgr2trlspth  29737  cyclnumvtx  29776  cyclnspth  29777  crctcshwlkn0lem3  29788  wwlksn  29813  wspthneq1eq2  29836  wwlksm1edg  29857  wwlksnred  29868  wwlksnextfun  29874  wwlksnextinj  29875  wwlksnextproplem3  29887  wspthsnonn0vne  29893  wspn0  29900  rusgrnumwwlk  29951  clwwlkccatlem  29964  umgrclwwlkge2  29966  clwlkclwwlklem2  29975  clwlkclwwlklem3  29976  clwwisshclwws  29990  clwwisshclwwsn  29991  clwwlkn1loopb  30018  wwlksext2clwwlk  30032  wwlksubclwwlk  30033  clwwlknonex2lem2  30083  upgr3v3e3cycl  30155  uhgr3cyclex  30157  upgr4cycl4dv4e  30160  eupth2lem3lem4  30206  eupth2lem3lem7  30209  eupth2  30214  eulerpath  30216  nfrgr2v  30247  frgr3vlem1  30248  3vfriswmgr  30253  1to2vfriswmgr  30254  1to3vfriswmgr  30255  3cyclfrgrrn1  30260  3cyclfrgrrn  30261  3cyclfrgrrn2  30262  4cycl2vnunb  30265  frgrncvvdeqlem2  30275  frgrncvvdeqlem8  30281  frgrncvvdeqlem9  30282  frgrwopreglem4a  30285  frgrwopreglem5lem  30295  frgrwopreglem5ALT  30297  frgrregorufr0  30299  frgr2wwlk1  30304  frgr2wwlkeqm  30306  fusgr2wsp2nb  30309  2wspmdisj  30312  frrusgrord  30316  numclwwlk1lem2f1  30332  numclwlk1  30346  frgrreggt1  30368  friendshipgt3  30373  hlim2  31167  elnlfn  31903  stle0i  32214  hstrbi  32241  spansncv2  32268  h1da  32324  fmptcof2  32634  sgn3da  32812  xreceu  32897  domnprodn0  33237  1arithufdlem3  33506  1arithufdlem4  33507  tpr2rico  33920  hasheuni  34093  ismeas  34207  sseqp1  34403  rrvsum  34462  dstfrvunirn  34483  signstfvc  34582  bnj607  34923  bnj1145  35000  bnj1204  35019  fineqvrep  35125  fineqvnttrclselem1  35129  onvf1odlem4  35138  fisshasheq  35147  subgrwlk  35164  subfacp1lem6  35217  cvmlift2lem12  35346  cvmlift3lem4  35354  satfrnmapom  35402  sat1el2xp  35411  satffunlem2  35440  satffun  35441  mrsubvrs  35554  climuzcnv  35703  iprodefisumlem  35772  dfon2lem9  35824  linethru  36186  elhf2  36208  finminlem  36351  fnessref  36390  neibastop2lem  36393  fnemeet2  36400  nndivsub  36490  bj-xpnzex  36992  bj-elpwg  37085  bj-epelg  37101  mptsnunlem  37371  dissneqlem  37373  topdifinffinlem  37380  iooelexlt  37395  domalom  37437  fvineqsneq  37445  wl-exeq  37567  wl-ax11-lem3  37620  matunitlindflem1  37655  poimirlem22  37681  poimirlem26  37685  poimirlem28  37687  poimirlem29  37688  poimirlem32  37691  heicant  37694  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  cover2  37754  upixp  37768  sdclem2  37781  fdc  37784  seqpo  37786  metf1o  37794  mettrifi  37796  sstotbnd3  37815  heibor1lem  37848  heiborlem5  37854  heibor  37860  bfplem1  37861  elghomlem2OLD  37925  grpokerinj  37932  isrngo  37936  rngodm1dm2  37971  ispridl2  38077  exlimddvf  38160  lssatle  39053  4atexlemex4  40111  uzindd  42009  evl1gprodd  42149  sn-axprlem3  42249  redvmptabs  42392  sn-sup3d  42524  mzpsubst  42780  jm2.18  43020  wepwsolem  43074  oaabsb  43326  oacl2g  43362  ofoafg  43386  ofoaid1  43390  ofoaid2  43391  naddonnn  43427  iunrelexp0  43734  relexpmulg  43742  cnvtrclfv  43756  clsk1indlem3  44075  grucollcld  44292  inaex  44329  dvgrat  44344  radcnvrat  44346  csbxpgVD  44925  sineq0ALT  44968  trfr  44994  relwf  44999  pwclaxpow  45016  omssaxinf2  45020  islptre  45658  iblspltprt  46010  stoweidlem2  46039  stoweidlem17  46054  stoweidlem21  46058  2reuimp0  47144  2reuimp  47145  afveu  47183  funbrafv  47188  ndmaovass  47236  afv2eu  47268  tz6.12c-afv2  47272  funop1  47313  f1oresf1o2  47321  fvmptrabdm  47323  nltle2tri  47343  2elfz2melfz  47348  fsummsndifre  47402  fsumsplitsndif  47403  fsummmodsndifre  47404  fsummmodsnunz  47405  elsetpreimafvssdm  47416  uniimaelsetpreimafv  47426  imasetpreimafvbijlemfv1  47433  iccpartiltu  47452  iccpartigtl  47453  iccpartleu  47458  iccpartgel  47459  iccpartrn  47460  iccpartiun  47464  icceuelpart  47466  iccpartnel  47468  fargshiftf  47470  fargshiftf1  47471  ichnfb  47495  elsprel  47505  prsprel  47517  sprsymrelfo  47527  paireqne  47541  sbcpr  47551  reupr  47552  fmtnoinf  47566  odz2prm2pw  47593  lighneallem4  47640  lighneal  47641  requad1  47652  requad2  47653  evensumeven  47737  even3prm2  47749  gbowgt5  47792  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  bgoldbnnsum3prm  47834  bgoldbtbndlem2  47836  bgoldbtbndlem4  47838  bgoldbtbnd  47839  dfsclnbgr6  47888  grimco  47919  cycl3grtri  47977  isubgr3stgrlem6  48001  gricgrlic  48048  gpgedgvtx0  48091  gpgprismgr4cycllem3  48127  pgnbgreunbgrlem5  48153  clcllaw  48221  rngccatidALTV  48302  ringccatidALTV  48336  scmsuppss  48401  gsumlsscl  48410  ply1mulgsumlem2  48418  lincvalsc0  48452  linc0scn0  48454  lincdifsn  48455  linc1  48456  lincellss  48457  lincsum  48460  lincscm  48461  lincsumcl  48462  lcoss  48467  lincext3  48487  lindslinindimp2lem4  48492  lindslinindsimp2lem5  48493  lindslinindsimp2  48494  lindsrng01  48499  snlindsntor  48502  lincresunit3lem2  48511  lincresunit3  48512  islindeps2  48514  blengt1fldiv2p1  48624  2arymaptf1  48684  resum2sqorgt0  48740  reorelicc  48741  rrx2plordisom  48754  rrx2linest  48773  rrxsphere  48779  line2ylem  48782  itsclc0xyqsol  48799  itscnhlinecirc02p  48816  mo0sn  48846  thincn0eu  49462