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  581  animpimp2impd  847  4casesdan  1042  dedlema  1046  dedlemb  1047  sbiedvw  2101  mo4  2566  2moswapv  2629  2moswap  2644  2mosOLD  2650  2eu2  2653  pm2.61ne  3017  nelelne  3031  r19.21be  3230  rspcebdv  3558  2reu2  3836  csbie2df  4383  minel  4406  uneqdifeq  4432  raltpd  4725  ssunsn2  4770  opthprneg  4808  ssuni  4875  uniss2  4884  elpwuni  5047  intss2  5050  disjord  5074  elpw2g  5274  elssabg  5284  axprlem3OLD  5371  axprlem4OLD  5372  axprlem5OLD  5373  axprglem  5378  oteqex  5454  otsndisj  5473  otiunsndisj  5474  epelg  5532  wereu  5627  relop  5805  riinint  5927  sotri3  6093  unixpid  6248  reuop  6257  ordtr2  6368  ordsssuc2  6416  iotan0  6488  funopg  6532  fun  6702  fvmptnf  6970  fvn0ssdmfun  7026  eldmrexrnb  7044  fmptco  7082  fnressn  7112  fressnfv  7114  fprb  7149  fvtp2g  7154  fvtp3g  7155  fconst2g  7158  fntpb  7164  f1dom3el3dif  7224  f1ounsn  7227  isores3  7290  isoselem  7296  oprabv  7427  eloprabga  7476  sorpsscmpl  7688  difex2  7714  ordpwsuc  7766  ordsucun  7776  limuni3  7803  trom  7826  fo1stres  7968  poxp  8078  soxp  8079  xpord3inddlem  8104  soseq  8109  suppimacnv  8124  fsuppeq  8125  funsssuppss  8140  brtpos2  8182  frrlem8  8243  fpr2a  8252  onnseq  8284  smores  8292  smofvon2  8296  tfrlem1  8315  oacl  8470  omcl  8471  oecl  8472  oawordri  8485  oalimcl  8495  oaass  8496  oarec  8497  omwordri  8507  omeulem1  8517  omeulem2  8518  oeordi  8523  oeworde  8529  oeoelem  8534  nnacl  8547  nnmcl  8548  nnecl  8549  nnacom  8553  nnaass  8558  nnmsucr  8561  nnmordi  8567  omabs  8587  cofonr  8610  naddunif  8629  iiner  8736  elpmg  8790  fsetfcdm  8807  fsetprcnex  8809  pmss12g  8817  mapfvd  8827  f1domg  8918  ssdomg  8947  undom  9003  domtriord  9061  ssnnfi  9104  fnfi  9112  enfi  9121  php  9141  sdom1  9160  1sdom2dom  9164  fisseneq  9173  isinf  9175  dif1ennnALT  9187  findcard3  9193  frfi  9195  difinf  9221  imafiOLD  9226  iunfi  9253  fsuppunfi  9301  fsuppres  9306  ffsuppbi  9311  elfi2  9327  marypha1lem  9346  marypha1  9347  oiexg  9450  wemapso2  9468  harword  9478  brwdom  9482  unxpwdom  9504  en3lplem1  9533  inf3lemd  9548  inf3lem5  9553  cantnfval2  9590  cantnfle  9592  cantnflt  9593  cnfcom  9621  tcmin  9660  frr2  9684  r1sdom  9698  rankxplim3  9805  cardidm  9883  cardmin2  9923  infxpenlem  9935  fseqenlem1  9946  numacn  9971  alephordi  9996  iscard3  10015  alephinit  10017  carduniima  10018  iunfictbso  10036  dfac5  10051  dfac12lem3  10068  nnadju  10120  pwsdompw  10125  pwdjudom  10137  cflim2  10185  cfslb2n  10190  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  alephsing  10198  infpssALT  10235  fin23lem34  10268  isf32lem2  10276  isf32lem10  10284  isf32lem12  10286  isfin1-2  10307  hsmexlem4  10351  axcc2lem  10358  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ac6num  10401  ac6s  10406  zorn2lem7  10424  ttukeylem5  10435  imadomg  10456  iundom2g  10462  ondomon  10485  ficard  10487  konigthlem  10491  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  axregndlem1  10525  axregnd  10527  pwfseqlem3  10583  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  inawinalem  10612  gchina  10622  wuncval2  10670  tsk0  10686  tskxpss  10695  inatsk  10701  tskuni  10706  gruina  10741  grothac  10753  addclpi  10815  addnidpi  10824  nqereu  10852  mulcanenq  10883  genpnnp  10928  nqpr  10937  prlem934  10956  reclem2pr  10971  suplem1pr  10975  supsrlem  11034  axpre-sup  11092  1re  11144  dedekindle  11310  00id  11321  receu  11795  sup3  12113  infrelb  12141  peano5nni  12177  nnindd  12194  nnaddcl  12197  zrevaddcl  12572  nzadd  12575  zdiv  12599  nneo  12613  zeo2  12616  nn0indd  12626  fzind  12627  fnn0ind  12628  fzindd  12631  uzwo  12861  lbzbi  12886  nn01to3  12891  qrevaddcl  12921  irradd  12923  irrmul  12924  ltsubrp  12980  ltaddrp  12981  xnn0xaddcl  13187  xnn0xadd0  13199  icoshft  13426  fzen  13495  elfzm11  13549  uzsplit  13550  elfzom1elp1fzo  13687  fzoopth  13717  injresinjlem  13745  injresinj  13746  modifeq2int  13895  modsumfzodifsn  13906  om2uzlti  13912  ssnn0fi  13947  fsuppmapnn0fiub0  13955  mptnn0fsuppr  13961  seqcaopr3  13999  seqf1olem2a  14002  seqf1o  14005  ser1const  14020  expadd  14066  expmul  14069  leexp1a  14137  faccl  14245  facdiv  14249  faclbnd  14252  faclbnd4lem4  14258  hasheqf1oi  14313  hashgadd  14339  hashinfxadd  14347  hashunx  14348  hashunsng  14354  elprchashprn2  14358  hashss  14371  hash1snb  14381  hashmap  14397  hashf1lem2  14418  hashf1  14419  seqcoll  14426  hashle2pr  14439  hashdmpropge2  14445  hashge3el3dif  14449  hash1to3  14454  fundmge2nop0  14464  fi1uzind  14469  brfi1indALT  14472  sswrd  14484  swrdnd2  14618  swrdnnn0nd  14619  swrdnd0  14620  swrdwrdsymb  14625  pfxnd0  14651  swrdswrdlem  14666  swrdswrd  14667  wrd2ind  14685  swrdccatin1  14687  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccat3  14696  repsdf2  14740  repswswrd  14746  cshw0  14756  cshwcl  14760  cshwlen  14761  cshf1  14772  swrdco  14799  relexpsucnnl  14992  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  rtrclind  15027  shftlem  15030  caubnd  15321  reusq0  15427  rlimcld2  15540  o1dif  15592  climub  15624  climserle  15625  iseraltlem2  15645  sumss  15686  fsumzcl2  15701  fsummsnunz  15716  fsumsplitsnun  15717  fsum2d  15733  modfsummods  15756  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  climcndslem1  15814  climcndslem2  15815  cvgrat  15848  clim2prod  15853  prodfn0  15859  prodfrec  15860  ntrivcvg  15862  prodmo  15901  fprodss  15913  fprodabs  15939  fprodn0  15944  fprod2d  15946  fprodefsum  16060  ruclem8  16204  ruclem9  16205  dvdsmod0  16227  dvds2ln  16258  dvdsaddre2b  16276  dvdslelem  16278  dvdsdivcl  16285  alzdvds  16289  mod2eq1n2dvds  16316  oddnn02np1  16317  nn0o1gt2  16350  nno  16351  sumeven  16356  sumodd  16357  pwp1fsum  16360  ndvdsadd  16379  bitsinv1  16411  sadcadd  16427  sadadd2  16429  saddisjlem  16433  smuval2  16451  smupvallem  16452  smu01lem  16454  smupval  16457  smueqlem  16459  smumullem  16461  gcddiv  16520  rplpwr  16527  nn0seqcvgd  16539  seq1st  16540  alginv  16544  algcvga  16548  algfx  16549  absprodnn  16587  isprm2  16651  isprm3  16652  prmind2  16654  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  17505  divsfval  17511  mreexexlem4d  17613  isssc  17787  initoeu1  17978  termoeu1  17985  istos  18382  chnfibg  18602  mgmcl  18611  sgrpidmnd  18707  frmdgsum  18830  smndex1mgm  18878  dfgrp3lem  19014  mhmmulg  19091  resghm2b  19209  gsumwrev  19341  elsymgbas  19349  symgextf1  19396  gsmsymgreqlem2  19406  gsmsymgreq  19407  odlem1  19510  odcl2  19540  gexlem1  19554  efgi2  19700  efginvrel2  19702  efgsrel  19709  cyggexb  19874  gsummulglem  19916  gsumzunsnd  19931  gsum2dlem2  19946  telgsums  19968  dmdprd  19975  dprdw  19987  ablfac1eulem  20049  srgpcomp  20199  rnghmmul  20429  nrhmzr  20514  lmodfopnelem1  20893  rmodislmodlem  20924  cnfldmulg  21384  cnfldexp  21385  nzerooringczr  21460  obslbs  21710  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  cply1mul  22261  coe1fzgsumdlem  22268  gsummoncoe1  22273  pf1ind  22320  evl1gsumdlem  22321  mat1dimcrng  22442  ma1repveval  22536  mulmarep1gsum2  22539  gsummatr01lem3  22622  cramerlem3  22654  decpmatmulsumfsupp  22738  mp2pm2mplem4  22774  pm2mpmhmlem1  22783  fvmptnn04if  22814  cayhamlem1  22831  fctop  22969  mretopd  23057  restopnb  23140  restdis  23143  tgcnp  23218  cncls2  23238  cncls  23239  cnntr  23240  cnsscnp  23244  cmpsub  23365  2ndcsep  23424  1stcelcls  23426  lfinpfin  23489  locfincmp  23491  comppfsc  23497  txcn  23591  txlm  23613  xkohaus  23618  qtopres  23663  haushmphlem  23752  cmphmph  23753  connhmph  23754  reghmph  23758  nrmhmph  23759  ptcmpfi  23778  reghaus  23790  fbssfi  23802  fbun  23805  fbfinnfr  23806  isfildlem  23822  fgcl  23843  cfinfil  23858  supfil  23860  ufinffr  23894  fin1aufil  23897  cnpflf  23966  alexsubALTlem3  24014  alexsubALT  24016  cnextfvval  24030  cnextcn  24032  tmdgsum  24060  tgphaus  24082  tgpt1  24083  mettri  24317  blssexps  24391  blssex  24392  mopni3  24459  metss  24473  psmetutop  24532  dscmet  24537  tngngp3  24621  rectbntr0  24798  metnrmlem1a  24824  fsumcn  24837  lmmbr  25225  caubl  25275  caublcls  25276  bcthlem5  25295  bcth3  25298  ovolunlem1a  25463  ovoliunnul  25474  finiunmbl  25511  voliunlem1  25517  volsuplem  25522  volsup  25523  dyadmax  25565  itgfsum  25794  dvnadd  25896  cpnord  25902  dvnfre  25919  dvmptfsum  25942  dvlip  25960  fta1g  26135  plyco  26206  dgrcolem1  26238  dgrco  26240  dvnply2  26253  plydivex  26263  plyexmo  26279  aannenlem1  26294  aaliou3lem2  26309  dvntaylp  26336  taylthlem1  26338  ulmval  26345  cxpmul2  26653  cxpsqrtth  26694  scvxcvx  26949  jensenlem2  26951  jensen  26952  ppiub  27167  bcmono  27240  bpos1lem  27245  bposlem5  27251  gausslemma2dlem6  27335  lgsquad2lem2  27348  2lgslem3  27367  2lgs  27370  2sqnn  27402  addsqnreup  27406  2sqreultblem  27411  2sqreunnltblem  27414  dchrisumlem1  27452  dchrisum0flb  27473  pntpbnd1  27549  pntlemf  27568  qabvle  27588  qabvexp  27589  ostthlem2  27591  ostth2lem2  27597  ltsval2  27620  ltssolem1  27639  negsprop  28027  mulsuniflem  28141  precsexlem6  28204  precsexlem7  28205  noseqind  28284  om2noseqlt  28291  n0addscl  28336  n0mulscl  28337  expsne0  28428  axeuclidlem  29031  axcontlem12  29044  umgrnloopv  29175  uhgredgrnv  29199  edglnl  29212  numedglnl  29213  usgruspgrb  29252  usgrnloopvALT  29270  usgredg2vlem2  29295  subupgr  29356  nbumgr  29416  uhgrnbgr0nb  29423  nbgr0edglem  29425  edgusgrnbfin  29442  nb3grprlem2  29450  uvtxnbgrvtx  29462  cplgrop  29506  cusgrfi  29527  fusgrmaxsize  29533  fusgrn0degnn0  29568  ewlkprop  29672  uspgr2wlkeq  29714  g0wlk0  29719  wlkreslem  29736  lfgriswlk  29755  upgrwlkdvde  29805  spthonepeq  29820  uhgrwkspth  29823  usgr2trlncl  29828  usgr2trlspth  29829  cyclnumvtx  29868  cyclnspth  29869  crctcshwlkn0lem3  29880  wwlksn  29905  wspthneq1eq2  29928  wwlksm1edg  29949  wwlksnred  29960  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextproplem3  29979  wspthsnonn0vne  29985  wspn0  29992  rusgrnumwwlk  30046  clwwlkccatlem  30059  umgrclwwlkge2  30061  clwlkclwwlklem2  30070  clwlkclwwlklem3  30071  clwwisshclwws  30085  clwwisshclwwsn  30086  clwwlkn1loopb  30113  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwlknonex2lem2  30178  upgr3v3e3cycl  30250  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  eupth2lem3lem4  30301  eupth2lem3lem7  30304  eupth2  30309  eulerpath  30311  nfrgr2v  30342  frgr3vlem1  30343  3vfriswmgr  30348  1to2vfriswmgr  30349  1to3vfriswmgr  30350  3cyclfrgrrn1  30355  3cyclfrgrrn  30356  3cyclfrgrrn2  30357  4cycl2vnunb  30360  frgrncvvdeqlem2  30370  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrwopreglem4a  30380  frgrwopreglem5lem  30390  frgrwopreglem5ALT  30392  frgrregorufr0  30394  frgr2wwlk1  30399  frgr2wwlkeqm  30401  fusgr2wsp2nb  30404  2wspmdisj  30407  frrusgrord  30411  numclwwlk1lem2f1  30427  numclwlk1  30441  frgrreggt1  30463  friendshipgt3  30468  hlim2  31263  elnlfn  31999  stle0i  32310  hstrbi  32337  spansncv2  32364  h1da  32420  fmptcof2  32730  sgn3da  32907  xreceu  32981  domnprodn0  33336  1arithufdlem3  33606  1arithufdlem4  33607  tpr2rico  34056  hasheuni  34229  ismeas  34343  sseqp1  34539  rrvsum  34598  dstfrvunirn  34619  signstfvc  34718  bnj607  35058  bnj1145  35135  bnj1204  35154  r1filim  35247  fineqvrep  35258  fineqvnttrclselem1  35265  onvf1odlem4  35288  fisshasheq  35297  subgrwlk  35314  subfacp1lem6  35367  cvmlift2lem12  35496  cvmlift3lem4  35504  satfrnmapom  35552  sat1el2xp  35561  satffunlem2  35590  satffun  35591  mrsubvrs  35704  climuzcnv  35853  iprodefisumlem  35922  dfon2lem9  35971  linethru  36335  elhf2  36357  finminlem  36500  fnessref  36539  neibastop2lem  36542  fnemeet2  36549  nndivsub  36639  mh-inf3f1  36723  bj-cbvew  36936  bj-xpnzex  37266  bj-elpwg  37359  bj-epelg  37375  bj-axseprep  37381  mptsnunlem  37654  dissneqlem  37656  topdifinffinlem  37663  iooelexlt  37678  domalom  37720  fvineqsneq  37728  wl-exeq  37859  matunitlindflem1  37937  poimirlem22  37963  poimirlem26  37967  poimirlem28  37969  poimirlem29  37970  poimirlem32  37973  heicant  37976  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  cover2  38036  upixp  38050  sdclem2  38063  fdc  38066  seqpo  38068  metf1o  38076  mettrifi  38078  sstotbnd3  38097  heibor1lem  38130  heiborlem5  38136  heibor  38142  bfplem1  38143  elghomlem2OLD  38207  grpokerinj  38214  isrngo  38218  rngodm1dm2  38253  ispridl2  38359  exlimddvf  38442  lssatle  39461  4atexlemex4  40519  uzindd  42417  evl1gprodd  42556  sn-axprlem3  42659  redvmptabs  42792  sn-sup3d  42937  mzpsubst  43180  jm2.18  43416  wepwsolem  43470  oaabsb  43722  oacl2g  43758  ofoafg  43782  ofoaid1  43786  ofoaid2  43787  naddonnn  43823  iunrelexp0  44129  relexpmulg  44137  cnvtrclfv  44151  clsk1indlem3  44470  grucollcld  44687  inaex  44724  dvgrat  44739  radcnvrat  44741  csbxpgVD  45320  sineq0ALT  45363  trfr  45389  relwf  45394  pwclaxpow  45411  omssaxinf2  45415  islptre  46049  iblspltprt  46401  stoweidlem2  46430  stoweidlem17  46445  stoweidlem21  46449  2reuimp0  47562  2reuimp  47563  afveu  47601  funbrafv  47606  ndmaovass  47654  afv2eu  47686  tz6.12c-afv2  47690  funop1  47731  f1oresf1o2  47739  fvmptrabdm  47741  nltle2tri  47761  2elfz2melfz  47766  fsummsndifre  47828  fsumsplitsndif  47829  fsummmodsndifre  47830  fsummmodsnunz  47831  elsetpreimafvssdm  47846  uniimaelsetpreimafv  47856  imasetpreimafvbijlemfv1  47863  iccpartiltu  47882  iccpartigtl  47883  iccpartleu  47888  iccpartgel  47889  iccpartrn  47890  iccpartiun  47894  icceuelpart  47896  iccpartnel  47898  fargshiftf  47900  fargshiftf1  47901  ichnfb  47925  elsprel  47935  prsprel  47947  sprsymrelfo  47957  paireqne  47971  sbcpr  47981  reupr  47982  fmtnoinf  47999  odz2prm2pw  48026  lighneallem4  48073  lighneal  48074  requad1  48098  requad2  48099  evensumeven  48183  even3prm2  48195  gbowgt5  48238  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  bgoldbtbndlem4  48284  bgoldbtbnd  48285  dfsclnbgr6  48334  grimco  48365  cycl3grtri  48423  isubgr3stgrlem6  48447  gricgrlic  48494  gpgedgvtx0  48537  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem5  48599  clcllaw  48667  rngccatidALTV  48748  ringccatidALTV  48782  scmsuppss  48847  gsumlsscl  48856  ply1mulgsumlem2  48863  lincvalsc0  48897  linc0scn0  48899  lincdifsn  48900  linc1  48901  lincellss  48902  lincsum  48905  lincscm  48906  lincsumcl  48907  lcoss  48912  lincext3  48932  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  lindsrng01  48944  snlindsntor  48947  lincresunit3lem2  48956  lincresunit3  48957  islindeps2  48959  blengt1fldiv2p1  49069  2arymaptf1  49129  resum2sqorgt0  49185  reorelicc  49186  rrx2plordisom  49199  rrx2linest  49218  rrxsphere  49224  line2ylem  49227  itsclc0xyqsol  49244  itscnhlinecirc02p  49261  mo0sn  49291  thincn0eu  49906