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  579  animpimp2impd  845  4casesdan  1042  dedlema  1046  dedlemb  1047  sbiedvw  2095  mo4  2569  2moswapv  2632  2moswap  2647  2mosOLD  2653  2eu2  2656  pm2.61ne  3033  nelelne  3047  r19.21be  3258  cbvraldva2  3356  rspcebdv  3629  2reu2  3920  csbie2df  4466  minel  4489  uneqdifeq  4516  raltpd  4806  ssunsn2  4852  opthprneg  4889  ssuni  4956  uniss2  4965  elpwuni  5128  intss2  5131  disjord  5155  elpw2g  5351  elssabg  5361  axprlem3  5443  axprlem4  5444  axprlem5  5445  oteqex  5519  otsndisj  5538  otiunsndisj  5539  epelg  5600  wereu  5696  relop  5875  riinint  5994  sotri3  6162  unixpid  6315  reuop  6324  ordtr2  6439  ordsssuc2  6486  iotan0  6563  funopg  6612  fun  6783  tz6.12cOLD  6947  fvmptnf  7051  fvn0ssdmfun  7108  eldmrexrnb  7126  fmptco  7163  fnressn  7192  fressnfv  7194  fprb  7231  fvtp2g  7236  fvtp3g  7237  fconst2g  7240  fntpb  7246  f1dom3el3dif  7306  isores3  7371  isoselem  7377  oprabv  7510  eloprabga  7558  eloprabgaOLD  7559  sorpsscmpl  7769  difex2  7795  ordpwsuc  7851  ordsucun  7861  limuni3  7889  trom  7912  fo1stres  8056  poxp  8169  soxp  8170  xpord3inddlem  8195  soseq  8200  suppimacnv  8215  fsuppeq  8216  funsssuppss  8231  brtpos2  8273  frrlem8  8334  fpr2a  8343  wfrlem12OLD  8376  onnseq  8400  smores  8408  smofvon2  8412  tfrlem1  8432  oacl  8591  omcl  8592  oecl  8593  oawordri  8606  oalimcl  8616  oaass  8617  oarec  8618  omwordri  8628  omeulem1  8638  omeulem2  8639  oeordi  8643  oeworde  8649  oeoelem  8654  nnacl  8667  nnmcl  8668  nnecl  8669  nnacom  8673  nnaass  8678  nnmsucr  8681  nnmordi  8687  omabs  8707  cofonr  8730  naddunif  8749  iiner  8847  elpmg  8901  fsetfcdm  8918  fsetprcnex  8920  pmss12g  8927  mapfvd  8937  f1domg  9032  ssdomg  9060  undom  9125  domtriord  9189  ssnnfi  9235  ssnnfiOLD  9236  fnfi  9244  enfi  9253  php  9273  phpOLD  9285  php3OLD  9287  sdom1  9305  1sdom2dom  9310  1sdomOLD  9312  fisseneq  9320  isinf  9323  isinfOLD  9324  dif1ennnALT  9339  findcard3  9346  findcard3OLD  9347  frfi  9349  difinf  9377  imafiOLD  9382  iunfi  9411  fsuppunfi  9457  fsuppres  9462  ffsuppbi  9467  elfi2  9483  marypha1lem  9502  marypha1  9503  oiexg  9604  wemapso2  9622  harword  9632  brwdom  9636  unxpwdom  9658  en3lplem1  9681  inf3lemd  9696  inf3lem5  9701  cantnfval2  9738  cantnfle  9740  cantnflt  9741  cnfcom  9769  tcmin  9810  frr2  9829  r1sdom  9843  rankxplim3  9950  cardidm  10028  cardmin2  10068  infxpenlem  10082  fseqenlem1  10093  numacn  10118  alephordi  10143  iscard3  10162  alephinit  10164  carduniima  10165  iunfictbso  10183  dfac5  10198  dfac12lem3  10215  nnadju  10267  pwsdompw  10272  pwdjudom  10284  cflim2  10332  cfslb2n  10337  cofsmo  10338  cfsmolem  10339  cfcoflem  10341  alephsing  10345  infpssALT  10382  fin23lem34  10415  isf32lem2  10423  isf32lem10  10431  isf32lem12  10433  isfin1-2  10454  hsmexlem4  10498  axcc2lem  10505  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  ac6num  10548  ac6s  10553  zorn2lem7  10571  ttukeylem5  10582  imadomg  10603  iundom2g  10609  ondomon  10632  ficard  10634  konigthlem  10637  alephreg  10651  pwcfsdom  10652  cfpwsdom  10653  axregndlem1  10671  axregnd  10673  pwfseqlem3  10729  pwxpndom2  10734  pwxpndom  10735  pwdjundom  10736  inawinalem  10758  gchina  10768  wuncval2  10816  tsk0  10832  tskxpss  10841  inatsk  10847  tskuni  10852  gruina  10887  grothac  10899  addclpi  10961  addnidpi  10970  nqereu  10998  mulcanenq  11029  genpnnp  11074  nqpr  11083  prlem934  11102  reclem2pr  11117  suplem1pr  11121  supsrlem  11180  axpre-sup  11238  1re  11290  dedekindle  11454  00id  11465  receu  11935  sup3  12252  infrelb  12280  peano5nni  12296  nnindd  12313  nnaddcl  12316  zrevaddcl  12688  nzadd  12691  zdiv  12713  nneo  12727  zeo2  12730  nn0indd  12740  fzind  12741  fnn0ind  12742  fzindd  12745  uzwo  12976  lbzbi  13001  nn01to3  13006  qrevaddcl  13036  irradd  13038  irrmul  13039  ltsubrp  13093  ltaddrp  13094  xnn0xaddcl  13297  xnn0xadd0  13309  icoshft  13533  fzen  13601  elfzm11  13655  uzsplit  13656  elfzoext  13773  elfzom1elp1fzo  13783  fzoopth  13812  injresinjlem  13837  injresinj  13838  modifeq2int  13984  modsumfzodifsn  13995  om2uzlti  14001  ssnn0fi  14036  fsuppmapnn0fiub0  14044  mptnn0fsuppr  14050  seqcaopr3  14088  seqf1olem2a  14091  seqf1o  14094  ser1const  14109  expadd  14155  expmul  14158  leexp1a  14225  faccl  14332  facdiv  14336  faclbnd  14339  faclbnd4lem4  14345  hasheqf1oi  14400  hashgadd  14426  hashinfxadd  14434  hashunx  14435  hashunsng  14441  elprchashprn2  14445  hashss  14458  hash1snb  14468  hashmap  14484  hashf1lem2  14505  hashf1  14506  seqcoll  14513  hashle2pr  14526  hashdmpropge2  14532  hashge3el3dif  14536  hash1to3  14541  fundmge2nop0  14551  fi1uzind  14556  brfi1indALT  14559  sswrd  14570  swrdnd2  14703  swrdnnn0nd  14704  swrdnd0  14705  swrdwrdsymb  14710  pfxnd0  14736  swrdswrdlem  14752  swrdswrd  14753  wrd2ind  14771  swrdccatin1  14773  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccat3  14782  repsdf2  14826  repswswrd  14832  cshw0  14842  cshwcl  14846  cshwlen  14847  cshf1  14858  swrdco  14886  relexpsucnnl  15079  rtrclreclem3  15109  rtrclreclem4  15110  relexpindlem  15112  rtrclind  15114  shftlem  15117  caubnd  15407  reusq0  15511  rlimcld2  15624  o1dif  15676  climub  15710  climserle  15711  iseraltlem2  15731  sumss  15772  fsumzcl2  15787  fsummsnunz  15802  fsumsplitsnun  15803  fsum2d  15819  modfsummods  15841  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  climcndslem1  15897  climcndslem2  15898  cvgrat  15931  clim2prod  15936  prodfn0  15942  prodfrec  15943  ntrivcvg  15945  prodmo  15984  fprodss  15996  fprodabs  16022  fprodn0  16027  fprod2d  16029  fprodefsum  16143  ruclem8  16285  ruclem9  16286  dvdsmod0  16308  dvds2ln  16337  dvdsaddre2b  16355  dvdslelem  16357  dvdsdivcl  16364  alzdvds  16368  mod2eq1n2dvds  16395  oddnn02np1  16396  nn0o1gt2  16429  nno  16430  sumeven  16435  sumodd  16436  pwp1fsum  16439  ndvdsadd  16458  bitsinv1  16488  sadcadd  16504  sadadd2  16506  saddisjlem  16510  smuval2  16528  smupvallem  16529  smu01lem  16531  smupval  16534  smueqlem  16536  smumullem  16538  gcddiv  16598  rplpwr  16605  nn0seqcvgd  16617  seq1st  16618  alginv  16622  algcvga  16626  algfx  16627  absprodnn  16665  isprm2  16729  isprm3  16730  prmind2  16732  maxprmfct  16756  prmdvdsexp  16762  pcmpt  16939  prmreclem4  16966  vdwmc2  17026  vdwlem10  17037  ramub2  17061  ramcl  17076  prmgaplem5  17102  prmgaplem8  17105  cshwshashlem1  17143  cshwshashlem3  17145  setsn0fun  17220  imasleval  17601  divsfval  17607  mreexexlem4d  17705  isssc  17881  initoeu1  18078  termoeu1  18085  istos  18488  mgmcl  18681  sgrpidmnd  18777  frmdgsum  18897  smndex1mgm  18942  dfgrp3lem  19078  mhmmulg  19155  resghm2b  19274  gsumwrev  19409  elsymgbas  19415  symgextf1  19463  gsmsymgreqlem2  19473  gsmsymgreq  19474  odlem1  19577  odcl2  19607  gexlem1  19621  efgi2  19767  efginvrel2  19769  efgsrel  19776  cyggexb  19941  gsummulglem  19983  gsumzunsnd  19998  gsum2dlem2  20013  telgsums  20035  dmdprd  20042  dprdw  20054  ablfac1eulem  20116  srgpcomp  20245  rnghmmul  20475  nrhmzr  20563  lmodfopnelem1  20918  rmodislmodlem  20949  cnfldmulg  21439  cnfldexp  21440  nzerooringczr  21514  obslbs  21773  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  cply1mul  22321  coe1fzgsumdlem  22328  gsummoncoe1  22333  pf1ind  22380  evl1gsumdlem  22381  mat1dimcrng  22504  ma1repveval  22598  mulmarep1gsum2  22601  gsummatr01lem3  22684  cramerlem3  22716  decpmatmulsumfsupp  22800  mp2pm2mplem4  22836  pm2mpmhmlem1  22845  fvmptnn04if  22876  cayhamlem1  22893  fctop  23032  mretopd  23121  restopnb  23204  restdis  23207  tgcnp  23282  cncls2  23302  cncls  23303  cnntr  23304  cnsscnp  23308  cmpsub  23429  2ndcsep  23488  1stcelcls  23490  lfinpfin  23553  locfincmp  23555  comppfsc  23561  txcn  23655  txlm  23677  xkohaus  23682  qtopres  23727  haushmphlem  23816  cmphmph  23817  connhmph  23818  reghmph  23822  nrmhmph  23823  ptcmpfi  23842  reghaus  23854  fbssfi  23866  fbun  23869  fbfinnfr  23870  isfildlem  23886  fgcl  23907  cfinfil  23922  supfil  23924  ufinffr  23958  fin1aufil  23961  cnpflf  24030  alexsubALTlem3  24078  alexsubALT  24080  cnextfvval  24094  cnextcn  24096  tmdgsum  24124  tgphaus  24146  tgpt1  24147  mettri  24383  blssexps  24457  blssex  24458  mopni3  24528  metss  24542  psmetutop  24601  dscmet  24606  tngngp3  24698  rectbntr0  24873  metnrmlem1a  24899  fsumcn  24913  lmmbr  25311  caubl  25361  caublcls  25362  bcthlem5  25381  bcth3  25384  ovolunlem1a  25550  ovoliunnul  25561  finiunmbl  25598  voliunlem1  25604  volsuplem  25609  volsup  25610  dyadmax  25652  itgfsum  25882  dvnadd  25985  cpnord  25991  dvnfre  26010  dvmptfsum  26033  dvlip  26052  fta1g  26229  plyco  26300  dgrcolem1  26333  dgrco  26335  dvnply2  26347  plydivex  26357  plyexmo  26373  aannenlem1  26388  aaliou3lem2  26403  dvntaylp  26431  taylthlem1  26433  ulmval  26441  cxpmul2  26749  cxpsqrtth  26790  scvxcvx  27047  jensenlem2  27049  jensen  27050  ppiub  27266  bcmono  27339  bpos1lem  27344  bposlem5  27350  gausslemma2dlem6  27434  lgsquad2lem2  27447  2lgslem3  27466  2lgs  27469  2sqnn  27501  addsqnreup  27505  2sqreultblem  27510  2sqreunnltblem  27513  dchrisumlem1  27551  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  qabvle  27687  qabvexp  27688  ostthlem2  27690  ostth2lem2  27696  sltval2  27719  sltsolem1  27738  negsprop  28085  mulsuniflem  28193  precsexlem6  28254  precsexlem7  28255  noseqind  28316  om2noseqlt  28323  n0addscl  28365  n0mulscl  28366  expsne0  28432  axeuclidlem  28995  axcontlem12  29008  umgrnloopv  29141  uhgredgrnv  29165  edglnl  29178  numedglnl  29179  usgruspgrb  29218  usgrnloopvALT  29236  usgredg2vlem2  29261  subupgr  29322  nbumgr  29382  uhgrnbgr0nb  29389  nbgr0edglem  29391  edgusgrnbfin  29408  nb3grprlem2  29416  uvtxnbgrvtx  29428  cplgrop  29472  cusgrfi  29494  fusgrmaxsize  29500  fusgrn0degnn0  29535  ewlkprop  29639  uspgr2wlkeq  29682  g0wlk0  29688  wlkreslem  29705  lfgriswlk  29724  upgrwlkdvde  29773  spthonepeq  29788  uhgrwkspth  29791  usgr2trlncl  29796  usgr2trlspth  29797  cyclnspth  29836  crctcshwlkn0lem3  29845  wwlksn  29870  wspthneq1eq2  29893  wwlksm1edg  29914  wwlksnred  29925  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextproplem3  29944  wspthsnonn0vne  29950  wspn0  29957  rusgrnumwwlk  30008  clwwlkccatlem  30021  umgrclwwlkge2  30023  clwlkclwwlklem2  30032  clwlkclwwlklem3  30033  clwwisshclwws  30047  clwwisshclwwsn  30048  clwwlkn1loopb  30075  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwlknonex2lem2  30140  upgr3v3e3cycl  30212  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  eupth2lem3lem4  30263  eupth2lem3lem7  30266  eupth2  30271  eulerpath  30273  nfrgr2v  30304  frgr3vlem1  30305  3vfriswmgr  30310  1to2vfriswmgr  30311  1to3vfriswmgr  30312  3cyclfrgrrn1  30317  3cyclfrgrrn  30318  3cyclfrgrrn2  30319  4cycl2vnunb  30322  frgrncvvdeqlem2  30332  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrwopreglem4a  30342  frgrwopreglem5lem  30352  frgrwopreglem5ALT  30354  frgrregorufr0  30356  frgr2wwlk1  30361  frgr2wwlkeqm  30363  fusgr2wsp2nb  30366  2wspmdisj  30369  frrusgrord  30373  numclwwlk1lem2f1  30389  numclwlk1  30403  frgrreggt1  30425  friendshipgt3  30430  hlim2  31224  elnlfn  31960  stle0i  32271  hstrbi  32298  spansncv2  32325  h1da  32381  fmptcof2  32675  xreceu  32886  domnprodn0  33247  1arithufdlem3  33539  1arithufdlem4  33540  tpr2rico  33858  hasheuni  34049  ismeas  34163  sseqp1  34360  rrvsum  34419  dstfrvunirn  34439  sgn3da  34506  signstfvc  34551  bnj607  34892  bnj1145  34969  bnj1204  34988  fineqvrep  35071  fisshasheq  35082  subgrwlk  35100  subfacp1lem6  35153  cvmlift2lem12  35282  cvmlift3lem4  35290  satfrnmapom  35338  sat1el2xp  35347  satffunlem2  35376  satffun  35377  mrsubvrs  35490  climuzcnv  35639  iprodefisumlem  35702  dfon2lem9  35755  linethru  36117  elhf2  36139  finminlem  36284  fnessref  36323  neibastop2lem  36326  fnemeet2  36333  nndivsub  36423  bj-xpnzex  36925  bj-elpwg  37018  bj-epelg  37034  mptsnunlem  37304  dissneqlem  37306  topdifinffinlem  37313  iooelexlt  37328  domalom  37370  fvineqsneq  37378  wl-exeq  37488  wl-ax11-lem3  37541  matunitlindflem1  37576  poimirlem22  37602  poimirlem26  37606  poimirlem28  37608  poimirlem29  37609  poimirlem32  37612  heicant  37615  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  cover2  37675  upixp  37689  sdclem2  37702  fdc  37705  seqpo  37707  metf1o  37715  mettrifi  37717  sstotbnd3  37736  heibor1lem  37769  heiborlem5  37775  heibor  37781  bfplem1  37782  elghomlem2OLD  37846  grpokerinj  37853  isrngo  37857  rngodm1dm2  37892  ispridl2  37998  exlimddvf  38081  lssatle  38971  4atexlemex4  40030  uzindd  41933  evl1gprodd  42074  sn-axprlem3  42210  sn-sup3d  42448  mzpsubst  42704  jm2.18  42945  wepwsolem  42999  oaabsb  43256  oacl2g  43292  ofoafg  43316  ofoaid1  43320  ofoaid2  43321  naddonnn  43357  iunrelexp0  43664  relexpmulg  43672  cnvtrclfv  43686  clsk1indlem3  44005  grucollcld  44229  inaex  44266  dvgrat  44281  radcnvrat  44283  csbxpgVD  44865  sineq0ALT  44908  islptre  45540  iblspltprt  45894  stoweidlem2  45923  stoweidlem17  45938  stoweidlem21  45942  2reuimp0  47029  2reuimp  47030  afveu  47068  funbrafv  47073  ndmaovass  47121  afv2eu  47153  tz6.12c-afv2  47157  funop1  47198  f1oresf1o2  47206  fvmptrabdm  47208  nltle2tri  47228  2elfz2melfz  47233  fsummsndifre  47246  fsumsplitsndif  47247  fsummmodsndifre  47248  fsummmodsnunz  47249  elsetpreimafvssdm  47260  uniimaelsetpreimafv  47270  imasetpreimafvbijlemfv1  47277  iccpartiltu  47296  iccpartigtl  47297  iccpartleu  47302  iccpartgel  47303  iccpartrn  47304  iccpartiun  47308  icceuelpart  47310  iccpartnel  47312  fargshiftf  47314  fargshiftf1  47315  ichnfb  47339  elsprel  47349  prsprel  47361  sprsymrelfo  47371  paireqne  47385  sbcpr  47395  reupr  47396  fmtnoinf  47410  odz2prm2pw  47437  lighneallem4  47484  lighneal  47485  requad1  47496  requad2  47497  evensumeven  47581  even3prm2  47593  gbowgt5  47636  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem4  47682  bgoldbtbnd  47683  dfsclnbgr6  47730  uspgrimprop  47757  grimco  47764  gricgrlic  47835  clcllaw  47914  rngccatidALTV  47995  ringccatidALTV  48029  scmsuppss  48097  gsumlsscl  48108  ply1mulgsumlem2  48116  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  linc1  48154  lincellss  48155  lincsum  48158  lincscm  48159  lincsumcl  48160  lcoss  48165  lincext3  48185  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lindsrng01  48197  snlindsntor  48200  lincresunit3lem2  48209  lincresunit3  48210  islindeps2  48212  blengt1fldiv2p1  48327  2arymaptf1  48387  resum2sqorgt0  48443  reorelicc  48444  rrx2plordisom  48457  rrx2linest  48476  rrxsphere  48482  line2ylem  48485  itsclc0xyqsol  48502  itscnhlinecirc02p  48519  mo0sn  48547  thincn0eu  48699