Theorem expcom 418

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ancoms  463  pm3.21  476  sylan  591  animpimp2impd  859  4casesdan  1055  dedlema  1059  dedlemb  1060  sbiedvw  2132  mo4  2596  2moswapv  2659  2moswap  2674  2eu2  2682  pm2.61ne  3045  nelelne  3059  r19.21be  3258  rspcebdv  3578  2reu2  3854  csbie2df  4400  minel  4423  uneqdifeq  4449  raltpd  4743  ssunsn2  4788  opthprneg  4826  ssuni  4894  uniss2  4903  elpwuni  5067  intss2  5070  disjord  5094  elpw2g  5294  elssabg  5304  axprlem3OLD  5391  axprlem4OLD  5392  axprlem5OLD  5393  axprglem  5398  oteqex  5474  otsndisj  5493  otiunsndisj  5494  epelg  5553  wereu  5648  relop  5827  riinint  5953  sotri3  6121  unixpid  6275  reuop  6284  ordtr2  6395  ordsssuc2  6443  iotan0  6515  funopg  6559  fun  6730  fvmptnf  7002  fvn0ssdmfun  7059  eldmrexrnb  7077  fmptco  7115  fnressn  7145  fressnfv  7147  fprb  7182  fvtp2g  7187  fvtp3g  7188  fconst2g  7191  fntpb  7197  f1dom3el3dif  7257  f1ounsn  7260  isores3  7323  isoselem  7329  oprabv  7460  eloprabga  7509  sorpsscmpl  7721  difex2  7747  ordpwsuc  7799  ordsucun  7809  limuni3  7836  trom  7859  fo1stres  8000  poxp  8112  soxp  8113  xpord3inddlem  8138  soseq  8143  suppimacnv  8158  fsuppeq  8159  funsssuppss  8174  brtpos2  8216  frrlem8  8278  fpr2a  8287  onnseq  8319  smores  8327  smofvon2  8331  tfrlem1  8350  oacl  8508  omcl  8509  oecl  8510  oawordri  8523  oalimcl  8533  oaass  8534  oarec  8535  omwordri  8545  omeulem1  8555  omeulem2  8556  oeordi  8561  oeworde  8567  oeoelem  8572  nnacl  8585  nnmcl  8586  nnecl  8587  nnacom  8591  nnaass  8596  nnmsucr  8599  nnmordi  8605  omabs  8625  cofonr  8648  naddunif  8668  iiner  8775  elpmg  8828  fsetfcdm  8845  fsetprcnex  8847  pmss12g  8855  mapfvd  8865  f1domg  8956  ssdomg  8985  undom  9041  domtriord  9099  ssnnfi  9142  fnfi  9150  enfi  9159  php  9179  sdom1  9198  1sdom2dom  9202  fisseneq  9211  isinf  9213  dif1ennnALT  9225  findcard3  9231  frfi  9233  difinf  9259  iunfi  9288  fsuppunfi  9336  fsuppres  9341  ffsuppbi  9346  elfi2  9362  marypha1lem  9381  marypha1  9382  oiexg  9485  wemapso2  9503  harword  9513  brwdom  9517  unxpwdom  9539  en3lplem1  9569  inf3lemd  9584  inf3lem5  9589  cantnfval2  9626  cantnfle  9628  cantnflt  9629  cnfcom  9657  tcmin  9696  frr2  9720  r1sdom  9734  rankxplim3  9841  cardidm  9933  cardmin2  9973  infxpenlem  9985  fseqenlem1  9996  numacn  10021  alephordi  10046  iscard3  10065  alephinit  10067  carduniima  10068  iunfictbso  10086  dfac5  10100  dfac12lem3  10117  nnadju  10169  pwsdompw  10174  pwdjudom  10186  cflim2  10235  cfslb2n  10240  cofsmo  10241  cfsmolem  10242  cfcoflem  10244  alephsing  10248  infpssALT  10285  fin23lem34  10318  isf32lem2  10326  isf32lem10  10334  isf32lem12  10336  isfin1-2  10357  hsmexlem4  10401  axcc2lem  10408  domtriomlem  10414  axdc2lem  10420  axdc3lem2  10423  axdc3lem4  10425  axdc4lem  10427  axcclem  10429  ac6num  10451  ac6s  10456  zorn2lem7  10474  ttukeylem5  10485  imadomg  10506  iundom2g  10512  ondomon  10535  ficard  10537  konigthlem  10541  alephreg  10555  pwcfsdom  10556  cfpwsdom  10557  axregndlem1  10575  axregnd  10577  pwfseqlem3  10633  pwxpndom2  10638  pwxpndom  10639  pwdjundom  10640  inawinalem  10662  gchina  10672  wuncval2  10720  tsk0  10736  tskxpss  10745  inatsk  10751  tskuni  10756  gruina  10791  grothac  10803  addclpi  10865  addnidpi  10874  nqereu  10902  mulcanenq  10933  genpnnp  10978  nqpr  10987  prlem934  11006  reclem2pr  11021  suplem1pr  11025  supsrlem  11084  axpre-sup  11142  1re  11196  dedekindle  11362  00id  11373  receu  11847  sup3  12163  infrelb  12191  peano5nni  12227  nnindd  12244  nnaddcl  12247  zrevaddcl  12630  nzadd  12633  zdiv  12657  nneo  12671  zeo2  12674  nn0indd  12684  fzind  12685  fnn0ind  12686  fzindd  12689  uzwo  12926  lbzbi  12951  nn01to3  12956  qrevaddcl  12986  irradd  12988  irrmul  12989  ltsubrp  13045  ltaddrp  13046  xnn0xaddcl  13252  xnn0xadd0  13264  icoshft  13491  fzen  13560  elfzm11  13614  uzsplit  13615  elfzom1elp1fzo  13752  fzoopth  13782  injresinjlem  13810  injresinj  13811  modifeq2int  13960  modsumfzodifsn  13971  om2uzlti  13977  ssnn0fi  14012  fsuppmapnn0fiub0  14020  mptnn0fsuppr  14026  seqcaopr3  14064  seqf1olem2a  14067  seqf1o  14070  ser1const  14085  expadd  14131  expmul  14134  leexp1a  14202  faccl  14310  facdiv  14314  faclbnd  14317  faclbnd4lem4  14323  hasheqf1oi  14378  hashgadd  14404  hashinfxadd  14412  hashunx  14413  hashunsng  14419  elprchashprn2  14423  hashss  14436  hash1snb  14446  hashmap  14462  hashf1lem2  14483  hashf1  14484  seqcoll  14491  hashle2pr  14504  hashdmpropge2  14510  hashge3el3dif  14514  hash1to3  14519  fundmge2nop0  14529  fi1uzind  14534  brfi1indALT  14537  sswrd  14549  swrdnd2  14683  swrdnnn0nd  14684  swrdnd0  14685  swrdwrdsymb  14690  pfxnd0  14716  swrdswrdlem  14731  swrdswrd  14732  wrd2ind  14750  swrdccatin1  14752  swrdccatin2  14756  pfxccatin12lem2  14758  pfxccat3  14761  repsdf2  14805  repswswrd  14811  cshw0  14821  cshwcl  14825  cshwlen  14826  cshf1  14837  swrdco  14864  relexpsucnnl  15057  rtrclreclem3  15087  rtrclreclem4  15088  relexpindlem  15090  rtrclind  15092  shftlem  15095  sgn3da  15128  caubnd  15400  reusq0  15506  rlimcld2  15619  o1dif  15671  climub  15703  climserle  15704  iseraltlem2  15724  sumss  15765  fsumzcl2  15780  fsummsnunz  15795  fsumsplitsnun  15796  fsum2d  15812  modfsummods  15835  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  climcndslem1  15893  climcndslem2  15894  cvgrat  15927  clim2prod  15932  prodfn0  15938  prodfrec  15939  ntrivcvg  15941  prodmo  15980  fprodss  15992  fprodabs  16018  fprodn0  16023  fprod2d  16025  fprodefsum  16139  ruclem8  16283  ruclem9  16284  dvdsmod0  16306  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  16490  sadcadd  16506  sadadd2  16508  saddisjlem  16512  smuval2  16530  smupvallem  16531  smu01lem  16533  smupval  16536  smueqlem  16538  smumullem  16540  gcddiv  16599  rplpwr  16606  nn0seqcvgd  16618  seq1st  16619  alginv  16623  algcvga  16627  algfx  16628  absprodnn  16666  isprm2  16730  isprm3  16731  prmind2  16733  maxprmfct  16758  prmdvdsexp  16764  pcmpt  16942  prmreclem4  16969  vdwmc2  17029  vdwlem10  17040  ramub2  17064  ramcl  17079  prmgaplem5  17105  prmgaplem8  17108  cshwshashlem1  17145  cshwshashlem3  17147  setsn0fun  17223  imasleval  17585  divsfval  17591  mreexexlem4d  17693  isssc  17867  initoeu1  18058  termoeu1  18065  istos  18462  chnfibg  18682  mgmcl  18691  sgrpidmnd  18787  frmdgsum  18911  smndex1mgm  18959  dfgrp3lem  19095  mhmmulg  19172  resghm2b  19295  gsumwrev  19427  elsymgbas  19435  symgextf1  19482  gsmsymgreqlem2  19492  gsmsymgreq  19493  odlem1  19596  odcl2  19626  gexlem1  19640  efgi2  19786  efginvrel2  19788  efgsrel  19795  cyggexb  19960  gsummulglem  20002  gsumzunsnd  20017  gsum2dlem2  20032  telgsums  20054  dmdprd  20061  dprdw  20073  ablfac1eulem  20135  srgpcomp  20291  rnghmmul  20522  nrhmzr  20613  lmodfopnelem1  20988  rmodislmodlem  21019  cnfldmulg  21514  cnfldexp  21515  nzerooringczr  21590  obslbs  21840  mplcoe1  22148  mplcoe3  22149  mplcoe5  22151  cply1mul  22417  coe1fzgsumdlem  22424  gsummoncoe1  22429  pf1ind  22476  evl1gsumdlem  22477  mat1dimcrng  22595  ma1repveval  22689  mulmarep1gsum2  22692  gsummatr01lem3  22775  cramerlem3  22807  decpmatmulsumfsupp  22891  mp2pm2mplem4  22927  pm2mpmhmlem1  22936  fvmptnn04if  22967  cayhamlem1  22984  fctop  23122  mretopd  23210  restopnb  23293  restdis  23296  tgcnp  23371  cncls2  23391  cncls  23392  cnntr  23393  cnsscnp  23397  cmpsub  23518  2ndcsep  23577  1stcelcls  23579  lfinpfin  23642  locfincmp  23644  comppfsc  23650  txcn  23744  txlm  23766  xkohaus  23771  qtopres  23816  haushmphlem  23905  cmphmph  23906  connhmph  23907  reghmph  23911  nrmhmph  23912  ptcmpfi  23931  reghaus  23943  fbssfi  23955  fbun  23958  fbfinnfr  23959  isfildlem  23975  fgcl  23996  cfinfil  24011  supfil  24013  ufinffr  24047  fin1aufil  24050  cnpflf  24119  alexsubALTlem3  24167  alexsubALT  24169  cnextfvval  24183  cnextcn  24185  tmdgsum  24213  tgphaus  24235  tgpt1  24236  mettri  24470  blssexps  24544  blssex  24545  mopni3  24612  metss  24626  psmetutop  24685  dscmet  24690  tngngp3  24774  rectbntr0  24951  metnrmlem1a  24977  fsumcn  24990  lmmbr  25378  caubl  25428  caublcls  25429  bcthlem5  25448  bcth3  25451  ovolunlem1a  25616  ovoliunnul  25627  finiunmbl  25664  voliunlem1  25670  volsuplem  25675  volsup  25676  dyadmax  25718  itgfsum  25947  dvnadd  26049  cpnord  26055  dvnfre  26072  dvmptfsum  26095  dvlip  26113  fta1g  26288  plyco  26359  dgrcolem1  26391  dgrco  26393  dvnply2  26409  plydivex  26419  plyexmo  26435  aannenlem1  26450  aaliou3lem2  26465  dvntaylp  26492  taylthlem1  26494  ulmval  26501  cxpmul2  26812  cxpsqrtth  26853  scvxcvx  27108  jensenlem2  27110  jensen  27111  ppiub  27326  bcmono  27399  bpos1lem  27404  bposlem5  27410  gausslemma2dlem6  27494  lgsquad2lem2  27507  2lgslem3  27526  2lgs  27529  2sqnn  27561  addsqnreup  27565  2sqreultblem  27570  2sqreunnltblem  27573  dchrisumlem1  27611  dchrisum0flb  27632  pntpbnd1  27708  pntlemf  27727  qabvle  27747  qabvexp  27748  ostthlem2  27750  ostth2lem2  27756  ltsval2  27778  ltssolem1  27797  negsprop  28186  mulsuniflem  28300  precsexlem6  28363  precsexlem7  28364  noseqind  28443  om2noseqlt  28450  n0addscl  28495  n0mulscl  28496  expsne0  28587  axeuclidlem  29221  axcontlem12  29234  umgrnloopv  29365  uhgredgrnv  29389  edglnl  29402  numedglnl  29403  usgruspgrb  29442  usgrnloopvALT  29460  usgredg2vlem2  29485  subupgr  29546  nbumgr  29606  uhgrnbgr0nb  29613  nbgr0edglem  29615  edgusgrnbfin  29632  nb3grprlem2  29640  uvtxnbgrvtx  29652  cplgrop  29696  cusgrfi  29717  fusgrmaxsize  29723  fusgrn0degnn0  29758  ewlkprop  29862  uspgr2wlkeq  29904  g0wlk0  29909  wlkreslem  29926  lfgriswlk  29945  upgrwlkdvde  29995  spthonepeq  30010  uhgrwkspth  30013  usgr2trlncl  30018  usgr2trlspth  30019  cyclnumvtx  30058  cyclnspth  30059  crctcshwlkn0lem3  30070  wwlksn  30095  wspthneq1eq2  30118  wwlksm1edg  30139  wwlksnred  30150  wwlksnextfun  30156  wwlksnextinj  30157  wwlksnextproplem3  30169  wspthsnonn0vne  30175  wspn0  30182  rusgrnumwwlk  30236  clwwlkccatlem  30249  umgrclwwlkge2  30251  clwlkclwwlklem2  30260  clwlkclwwlklem3  30261  clwwisshclwws  30275  clwwisshclwwsn  30276  clwwlkn1loopb  30303  wwlksext2clwwlk  30317  wwlksubclwwlk  30318  clwwlknonex2lem2  30368  upgr3v3e3cycl  30440  uhgr3cyclex  30442  upgr4cycl4dv4e  30445  eupth2lem3lem4  30491  eupth2lem3lem7  30494  eupth2  30499  eulerpath  30501  nfrgr2v  30532  frgr3vlem1  30533  3vfriswmgr  30538  1to2vfriswmgr  30539  1to3vfriswmgr  30540  3cyclfrgrrn1  30545  3cyclfrgrrn  30546  3cyclfrgrrn2  30547  4cycl2vnunb  30550  frgrncvvdeqlem2  30560  frgrncvvdeqlem8  30566  frgrncvvdeqlem9  30567  frgrwopreglem4a  30570  frgrwopreglem5lem  30580  frgrwopreglem5ALT  30582  frgrregorufr0  30584  frgr2wwlk1  30589  frgr2wwlkeqm  30591  fusgr2wsp2nb  30594  2wspmdisj  30597  frrusgrord  30601  numclwwlk1lem2f1  30617  numclwlk1  30631  frgrreggt1  30653  friendshipgt3  30658  hlim2  31453  elnlfn  32189  stle0i  32500  hstrbi  32527  spansncv2  32554  h1da  32610  fmptcof2  32914  xreceu  33154  domnprodn0  33511  1arithufdlem3  33753  1arithufdlem4  33754  tpr2rico  34219  hasheuni  34392  ismeas  34506  sseqp1  34702  rrvsum  34761  dstfrvunirn  34782  signstfvc  34878  bnj607  35221  bnj1145  35298  bnj1204  35317  r1filim  35412  fineqvrep  35422  fineqvnttrclselem1  35429  onvf1odlem4  35461  vonf1oonfo  35470  fisshasheq  35477  subgrwlk  35495  subfacp1lem6  35548  cvmlift2lem12  35677  cvmlift3lem4  35685  satfrnmapom  35733  sat1el2xp  35742  satffunlem2  35771  satffun  35772  mrsubvrs  35885  climuzcnv  36034  iprodefisumlem  36103  dfon2lem9  36152  linethru  36516  elhf2  36538  finminlem  36691  fnessref  36730  neibastop2lem  36733  fnemeet2  36740  nndivsub  36830  mh-inf3f1  36914  bj-cbvew  37126  bj-xpnzex  37456  bj-elpwg  37549  bj-epelg  37565  bj-axseprep  37571  mptsnunlem  37844  dissneqlem  37846  topdifinffinlem  37853  iooelexlt  37868  domalom  37910  fvineqsneq  37918  wl-exeq  38049  matunitlindflem1  38127  poimirlem22  38153  poimirlem26  38157  poimirlem28  38159  poimirlem29  38160  poimirlem32  38163  heicant  38166  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  cover2  38226  upixp  38240  sdclem2  38253  fdc  38256  seqpo  38258  metf1o  38266  mettrifi  38268  sstotbnd3  38287  heibor1lem  38320  heiborlem5  38326  heibor  38332  bfplem1  38333  elghomlem2OLD  38397  grpokerinj  38404  isrngo  38408  rngodm1dm2  38443  ispridl2  38549  exlimddvf  38632  lssatle  39651  4atexlemex4  40709  uzindd  42607  evl1gprodd  42746  sn-axprlem3  42849  redvmptabs  42981  sn-sup3d  43126  mzpsubst  43341  jm2.18  43577  wepwsolem  43631  oaabsb  43883  oacl2g  43919  ofoafg  43943  ofoaid1  43947  ofoaid2  43948  naddonnn  43984  iunrelexp0  44290  relexpmulg  44298  cnvtrclfv  44312  clsk1indlem3  44631  grucollcld  44834  inaex  44871  dvgrat  44886  radcnvrat  44888  csbxpgVD  45467  sineq0ALT  45510  trfr  45536  relwf  45541  pwclaxpow  45558  omssaxinf2  45562  islptre  46193  iblspltprt  46545  stoweidlem2  46574  stoweidlem17  46589  stoweidlem21  46593  2reuimp0  47706  2reuimp  47707  afveu  47745  funbrafv  47750  ndmaovass  47798  afv2eu  47830  tz6.12c-afv2  47834  funop1  47875  f1oresf1o2  47883  fvmptrabdm  47885  nltle2tri  47905  2elfz2melfz  47910  fsummsndifre  47972  fsumsplitsndif  47973  fsummmodsndifre  47974  fsummmodsnunz  47975  elsetpreimafvssdm  47990  uniimaelsetpreimafv  48000  imasetpreimafvbijlemfv1  48007  iccpartiltu  48026  iccpartigtl  48027  iccpartleu  48032  iccpartgel  48033  iccpartrn  48034  iccpartiun  48038  icceuelpart  48040  iccpartnel  48042  fargshiftf  48044  fargshiftf1  48045  ichnfb  48069  elsprel  48079  prsprel  48091  sprsymrelfo  48101  paireqne  48115  sbcpr  48125  reupr  48126  fmtnoinf  48143  odz2prm2pw  48170  lighneallem4  48217  lighneal  48218  requad1  48242  requad2  48243  evensumeven  48327  even3prm2  48339  gbowgt5  48382  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  bgoldbnnsum3prm  48424  bgoldbtbndlem2  48426  bgoldbtbndlem4  48428  bgoldbtbnd  48429  dfsclnbgr6  48478  grimco  48509  cycl3grtri  48567  isubgr3stgrlem6  48591  gricgrlic  48638  gpgedgvtx0  48681  gpgprismgr4cycllem3  48717  pgnbgreunbgrlem5  48743  clcllaw  48811  rngccatidALTV  48892  ringccatidALTV  48926  scmsuppss  49002  gsumlsscl  49011  ply1mulgsumlem2  49018  lincvalsc0  49052  linc0scn0  49054  lincdifsn  49055  linc1  49056  lincellss  49057  lincsum  49060  lincscm  49061  lincsumcl  49062  lcoss  49067  lincext3  49087  lindslinindimp2lem4  49092  lindslinindsimp2lem5  49093  lindslinindsimp2  49094  lindsrng01  49099  snlindsntor  49102  lincresunit3lem2  49111  lincresunit3  49112  islindeps2  49114  blengt1fldiv2p1  49224  2arymaptf1  49284  resum2sqorgt0  49340  reorelicc  49341  rrx2plordisom  49354  rrx2linest  49373  rrxsphere  49379  line2ylem  49382  itsclc0xyqsol  49399  itscnhlinecirc02p  49416  mo0sn  49445  thincn0eu  50060