Theorem expcom 417

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ancoms  462  pm3.21  475  sylan  589  animpimp2impd  857  4casesdan  1052  dedlema  1056  dedlemb  1057  sbiedvw  2128  mo4  2592  2moswapv  2655  2moswap  2670  2eu2  2678  pm2.61ne  3041  nelelne  3055  r19.21be  3254  rspcebdv  3575  2reu2  3851  csbie2df  4396  minel  4419  uneqdifeq  4445  raltpd  4739  ssunsn2  4784  opthprneg  4822  ssuni  4890  uniss2  4899  elpwuni  5061  intss2  5064  disjord  5088  elpw2g  5288  elssabg  5298  axprlem3OLD  5385  axprlem4OLD  5386  axprlem5OLD  5387  axprglem  5392  oteqex  5468  otsndisj  5487  otiunsndisj  5488  epelg  5546  wereu  5641  relop  5820  riinint  5946  sotri3  6114  unixpid  6267  reuop  6276  ordtr2  6387  ordsssuc2  6435  iotan0  6507  funopg  6551  fun  6722  fvmptnf  6994  fvn0ssdmfun  7051  eldmrexrnb  7069  fmptco  7107  fnressn  7137  fressnfv  7139  fprb  7174  fvtp2g  7179  fvtp3g  7180  fconst2g  7183  fntpb  7189  f1dom3el3dif  7249  f1ounsn  7252  isores3  7315  isoselem  7321  oprabv  7452  eloprabga  7501  sorpsscmpl  7713  difex2  7739  ordpwsuc  7791  ordsucun  7801  limuni3  7828  trom  7851  fo1stres  7992  poxp  8103  soxp  8104  xpord3inddlem  8129  soseq  8134  suppimacnv  8149  fsuppeq  8150  funsssuppss  8165  brtpos2  8207  frrlem8  8269  fpr2a  8278  onnseq  8310  smores  8318  smofvon2  8322  tfrlem1  8341  oacl  8499  omcl  8500  oecl  8501  oawordri  8514  oalimcl  8524  oaass  8525  oarec  8526  omwordri  8536  omeulem1  8546  omeulem2  8547  oeordi  8552  oeworde  8558  oeoelem  8563  nnacl  8576  nnmcl  8577  nnecl  8578  nnacom  8582  nnaass  8587  nnmsucr  8590  nnmordi  8596  omabs  8616  cofonr  8639  naddunif  8659  iiner  8766  elpmg  8820  fsetfcdm  8837  fsetprcnex  8839  pmss12g  8847  mapfvd  8857  f1domg  8948  ssdomg  8977  undom  9033  domtriord  9091  ssnnfi  9134  fnfi  9142  enfi  9151  php  9171  sdom1  9190  1sdom2dom  9194  fisseneq  9203  isinf  9205  dif1ennnALT  9217  findcard3  9223  frfi  9225  difinf  9251  imafiOLD  9256  iunfi  9283  fsuppunfi  9331  fsuppres  9336  ffsuppbi  9341  elfi2  9357  marypha1lem  9376  marypha1  9377  oiexg  9480  wemapso2  9498  harword  9508  brwdom  9512  unxpwdom  9534  en3lplem1  9564  inf3lemd  9579  inf3lem5  9584  cantnfval2  9621  cantnfle  9623  cantnflt  9624  cnfcom  9652  tcmin  9691  frr2  9715  r1sdom  9729  rankxplim3  9836  cardidm  9914  cardmin2  9954  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  10217  cfslb2n  10222  cofsmo  10223  cfsmolem  10224  cfcoflem  10226  alephsing  10230  infpssALT  10267  fin23lem34  10300  isf32lem2  10308  isf32lem10  10316  isf32lem12  10318  isfin1-2  10339  hsmexlem4  10383  axcc2lem  10390  domtriomlem  10396  axdc2lem  10402  axdc3lem2  10405  axdc3lem4  10407  axdc4lem  10409  axcclem  10411  ac6num  10433  ac6s  10438  zorn2lem7  10456  ttukeylem5  10467  imadomg  10488  iundom2g  10494  ondomon  10517  ficard  10519  konigthlem  10523  alephreg  10537  pwcfsdom  10538  cfpwsdom  10539  axregndlem1  10557  axregnd  10559  pwfseqlem3  10615  pwxpndom2  10620  pwxpndom  10621  pwdjundom  10622  inawinalem  10644  gchina  10654  wuncval2  10702  tsk0  10718  tskxpss  10727  inatsk  10733  tskuni  10738  gruina  10773  grothac  10785  addclpi  10847  addnidpi  10856  nqereu  10884  mulcanenq  10915  genpnnp  10960  nqpr  10969  prlem934  10988  reclem2pr  11003  suplem1pr  11007  supsrlem  11066  axpre-sup  11124  1re  11178  dedekindle  11344  00id  11355  receu  11829  sup3  12146  infrelb  12174  peano5nni  12210  nnindd  12227  nnaddcl  12230  zrevaddcl  12613  nzadd  12616  zdiv  12640  nneo  12654  zeo2  12657  nn0indd  12667  fzind  12668  fnn0ind  12669  fzindd  12672  uzwo  12909  lbzbi  12934  nn01to3  12939  qrevaddcl  12969  irradd  12971  irrmul  12972  ltsubrp  13028  ltaddrp  13029  xnn0xaddcl  13235  xnn0xadd0  13247  icoshft  13474  fzen  13543  elfzm11  13597  uzsplit  13598  elfzom1elp1fzo  13735  fzoopth  13765  injresinjlem  13793  injresinj  13794  modifeq2int  13943  modsumfzodifsn  13954  om2uzlti  13960  ssnn0fi  13995  fsuppmapnn0fiub0  14003  mptnn0fsuppr  14009  seqcaopr3  14047  seqf1olem2a  14050  seqf1o  14053  ser1const  14068  expadd  14114  expmul  14117  leexp1a  14185  faccl  14293  facdiv  14297  faclbnd  14300  faclbnd4lem4  14306  hasheqf1oi  14361  hashgadd  14387  hashinfxadd  14395  hashunx  14396  hashunsng  14402  elprchashprn2  14406  hashss  14419  hash1snb  14429  hashmap  14445  hashf1lem2  14466  hashf1  14467  seqcoll  14474  hashle2pr  14487  hashdmpropge2  14493  hashge3el3dif  14497  hash1to3  14502  fundmge2nop0  14512  fi1uzind  14517  brfi1indALT  14520  sswrd  14532  swrdnd2  14666  swrdnnn0nd  14667  swrdnd0  14668  swrdwrdsymb  14673  pfxnd0  14699  swrdswrdlem  14714  swrdswrd  14715  wrd2ind  14733  swrdccatin1  14735  swrdccatin2  14739  pfxccatin12lem2  14741  pfxccat3  14744  repsdf2  14788  repswswrd  14794  cshw0  14804  cshwcl  14808  cshwlen  14809  cshf1  14820  swrdco  14847  relexpsucnnl  15040  rtrclreclem3  15070  rtrclreclem4  15071  relexpindlem  15073  rtrclind  15075  shftlem  15078  caubnd  15369  reusq0  15475  rlimcld2  15588  o1dif  15640  climub  15672  climserle  15673  iseraltlem2  15693  sumss  15734  fsumzcl2  15749  fsummsnunz  15764  fsumsplitsnun  15765  fsum2d  15781  modfsummods  15804  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  climcndslem1  15862  climcndslem2  15863  cvgrat  15896  clim2prod  15901  prodfn0  15907  prodfrec  15908  ntrivcvg  15910  prodmo  15949  fprodss  15961  fprodabs  15987  fprodn0  15992  fprod2d  15994  fprodefsum  16108  ruclem8  16252  ruclem9  16253  dvdsmod0  16275  dvds2ln  16306  dvdsaddre2b  16324  dvdslelem  16326  dvdsdivcl  16333  alzdvds  16337  mod2eq1n2dvds  16364  oddnn02np1  16365  nn0o1gt2  16398  nno  16399  sumeven  16404  sumodd  16405  pwp1fsum  16408  ndvdsadd  16427  bitsinv1  16459  sadcadd  16475  sadadd2  16477  saddisjlem  16481  smuval2  16499  smupvallem  16500  smu01lem  16502  smupval  16505  smueqlem  16507  smumullem  16509  gcddiv  16568  rplpwr  16575  nn0seqcvgd  16587  seq1st  16588  alginv  16592  algcvga  16596  algfx  16597  absprodnn  16635  isprm2  16699  isprm3  16700  prmind2  16702  maxprmfct  16727  prmdvdsexp  16733  pcmpt  16911  prmreclem4  16938  vdwmc2  16998  vdwlem10  17009  ramub2  17033  ramcl  17048  prmgaplem5  17074  prmgaplem8  17077  cshwshashlem1  17114  cshwshashlem3  17116  setsn0fun  17192  imasleval  17554  divsfval  17560  mreexexlem4d  17662  isssc  17836  initoeu1  18027  termoeu1  18034  istos  18431  chnfibg  18651  mgmcl  18660  sgrpidmnd  18756  frmdgsum  18879  smndex1mgm  18927  dfgrp3lem  19063  mhmmulg  19140  resghm2b  19257  gsumwrev  19389  elsymgbas  19397  symgextf1  19444  gsmsymgreqlem2  19454  gsmsymgreq  19455  odlem1  19558  odcl2  19588  gexlem1  19602  efgi2  19748  efginvrel2  19750  efgsrel  19757  cyggexb  19922  gsummulglem  19964  gsumzunsnd  19979  gsum2dlem2  19994  telgsums  20016  dmdprd  20023  dprdw  20035  ablfac1eulem  20097  srgpcomp  20247  rnghmmul  20477  nrhmzr  20566  lmodfopnelem1  20945  rmodislmodlem  20976  cnfldmulg  21436  cnfldexp  21437  nzerooringczr  21512  obslbs  21762  mplcoe1  22070  mplcoe3  22071  mplcoe5  22073  cply1mul  22339  coe1fzgsumdlem  22346  gsummoncoe1  22351  pf1ind  22398  evl1gsumdlem  22399  mat1dimcrng  22517  ma1repveval  22611  mulmarep1gsum2  22614  gsummatr01lem3  22697  cramerlem3  22729  decpmatmulsumfsupp  22813  mp2pm2mplem4  22849  pm2mpmhmlem1  22858  fvmptnn04if  22889  cayhamlem1  22906  fctop  23044  mretopd  23132  restopnb  23215  restdis  23218  tgcnp  23293  cncls2  23313  cncls  23314  cnntr  23315  cnsscnp  23319  cmpsub  23440  2ndcsep  23499  1stcelcls  23501  lfinpfin  23564  locfincmp  23566  comppfsc  23572  txcn  23666  txlm  23688  xkohaus  23693  qtopres  23738  haushmphlem  23827  cmphmph  23828  connhmph  23829  reghmph  23833  nrmhmph  23834  ptcmpfi  23853  reghaus  23865  fbssfi  23877  fbun  23880  fbfinnfr  23881  isfildlem  23897  fgcl  23918  cfinfil  23933  supfil  23935  ufinffr  23969  fin1aufil  23972  cnpflf  24041  alexsubALTlem3  24089  alexsubALT  24091  cnextfvval  24105  cnextcn  24107  tmdgsum  24135  tgphaus  24157  tgpt1  24158  mettri  24392  blssexps  24466  blssex  24467  mopni3  24534  metss  24548  psmetutop  24607  dscmet  24612  tngngp3  24696  rectbntr0  24873  metnrmlem1a  24899  fsumcn  24912  lmmbr  25300  caubl  25350  caublcls  25351  bcthlem5  25370  bcth3  25373  ovolunlem1a  25538  ovoliunnul  25549  finiunmbl  25586  voliunlem1  25592  volsuplem  25597  volsup  25598  dyadmax  25640  itgfsum  25869  dvnadd  25971  cpnord  25977  dvnfre  25994  dvmptfsum  26017  dvlip  26035  fta1g  26210  plyco  26281  dgrcolem1  26313  dgrco  26315  dvnply2  26328  plydivex  26338  plyexmo  26354  aannenlem1  26369  aaliou3lem2  26384  dvntaylp  26411  taylthlem1  26413  ulmval  26420  cxpmul2  26731  cxpsqrtth  26772  scvxcvx  27027  jensenlem2  27029  jensen  27030  ppiub  27245  bcmono  27318  bpos1lem  27323  bposlem5  27329  gausslemma2dlem6  27413  lgsquad2lem2  27426  2lgslem3  27445  2lgs  27448  2sqnn  27480  addsqnreup  27484  2sqreultblem  27489  2sqreunnltblem  27492  dchrisumlem1  27530  dchrisum0flb  27551  pntpbnd1  27627  pntlemf  27646  qabvle  27666  qabvexp  27667  ostthlem2  27669  ostth2lem2  27675  ltsval2  27697  ltssolem1  27716  negsprop  28105  mulsuniflem  28219  precsexlem6  28282  precsexlem7  28283  noseqind  28362  om2noseqlt  28369  n0addscl  28414  n0mulscl  28415  expsne0  28506  axeuclidlem  29109  axcontlem12  29122  umgrnloopv  29253  uhgredgrnv  29277  edglnl  29290  numedglnl  29291  usgruspgrb  29330  usgrnloopvALT  29348  usgredg2vlem2  29373  subupgr  29434  nbumgr  29494  uhgrnbgr0nb  29501  nbgr0edglem  29503  edgusgrnbfin  29520  nb3grprlem2  29528  uvtxnbgrvtx  29540  cplgrop  29584  cusgrfi  29605  fusgrmaxsize  29611  fusgrn0degnn0  29646  ewlkprop  29750  uspgr2wlkeq  29792  g0wlk0  29797  wlkreslem  29814  lfgriswlk  29833  upgrwlkdvde  29883  spthonepeq  29898  uhgrwkspth  29901  usgr2trlncl  29906  usgr2trlspth  29907  cyclnumvtx  29946  cyclnspth  29947  crctcshwlkn0lem3  29958  wwlksn  29983  wspthneq1eq2  30006  wwlksm1edg  30027  wwlksnred  30038  wwlksnextfun  30044  wwlksnextinj  30045  wwlksnextproplem3  30057  wspthsnonn0vne  30063  wspn0  30070  rusgrnumwwlk  30124  clwwlkccatlem  30137  umgrclwwlkge2  30139  clwlkclwwlklem2  30148  clwlkclwwlklem3  30149  clwwisshclwws  30163  clwwisshclwwsn  30164  clwwlkn1loopb  30191  wwlksext2clwwlk  30205  wwlksubclwwlk  30206  clwwlknonex2lem2  30256  upgr3v3e3cycl  30328  uhgr3cyclex  30330  upgr4cycl4dv4e  30333  eupth2lem3lem4  30379  eupth2lem3lem7  30382  eupth2  30387  eulerpath  30389  nfrgr2v  30420  frgr3vlem1  30421  3vfriswmgr  30426  1to2vfriswmgr  30427  1to3vfriswmgr  30428  3cyclfrgrrn1  30433  3cyclfrgrrn  30434  3cyclfrgrrn2  30435  4cycl2vnunb  30438  frgrncvvdeqlem2  30448  frgrncvvdeqlem8  30454  frgrncvvdeqlem9  30455  frgrwopreglem4a  30458  frgrwopreglem5lem  30468  frgrwopreglem5ALT  30470  frgrregorufr0  30472  frgr2wwlk1  30477  frgr2wwlkeqm  30479  fusgr2wsp2nb  30482  2wspmdisj  30485  frrusgrord  30489  numclwwlk1lem2f1  30505  numclwlk1  30519  frgrreggt1  30541  friendshipgt3  30546  hlim2  31341  elnlfn  32077  stle0i  32388  hstrbi  32415  spansncv2  32442  h1da  32498  fmptcof2  32809  sgn3da  32986  xreceu  33060  domnprodn0  33420  1arithufdlem3  33703  1arithufdlem4  33704  tpr2rico  34170  hasheuni  34343  ismeas  34457  sseqp1  34653  rrvsum  34712  dstfrvunirn  34733  signstfvc  34832  bnj607  35175  bnj1145  35252  bnj1204  35271  r1filim  35364  fineqvrep  35374  fineqvnttrclselem1  35381  onvf1odlem4  35413  vonf1oonfo  35422  fisshasheq  35429  subgrwlk  35446  subfacp1lem6  35499  cvmlift2lem12  35628  cvmlift3lem4  35636  satfrnmapom  35684  sat1el2xp  35693  satffunlem2  35722  satffun  35723  mrsubvrs  35836  climuzcnv  35985  iprodefisumlem  36054  dfon2lem9  36103  linethru  36467  elhf2  36489  finminlem  36642  fnessref  36681  neibastop2lem  36684  fnemeet2  36691  nndivsub  36781  mh-inf3f1  36865  bj-cbvew  37078  bj-xpnzex  37408  bj-elpwg  37501  bj-epelg  37517  bj-axseprep  37523  mptsnunlem  37796  dissneqlem  37798  topdifinffinlem  37805  iooelexlt  37820  domalom  37862  fvineqsneq  37870  wl-exeq  38001  matunitlindflem1  38079  poimirlem22  38105  poimirlem26  38109  poimirlem28  38111  poimirlem29  38112  poimirlem32  38115  heicant  38118  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  cover2  38178  upixp  38192  sdclem2  38205  fdc  38208  seqpo  38210  metf1o  38218  mettrifi  38220  sstotbnd3  38239  heibor1lem  38272  heiborlem5  38278  heibor  38284  bfplem1  38285  elghomlem2OLD  38349  grpokerinj  38356  isrngo  38360  rngodm1dm2  38395  ispridl2  38501  exlimddvf  38584  lssatle  39603  4atexlemex4  40661  uzindd  42559  evl1gprodd  42698  sn-axprlem3  42801  redvmptabs  42933  sn-sup3d  43078  mzpsubst  43293  jm2.18  43529  wepwsolem  43583  oaabsb  43835  oacl2g  43871  ofoafg  43895  ofoaid1  43899  ofoaid2  43900  naddonnn  43936  iunrelexp0  44242  relexpmulg  44250  cnvtrclfv  44264  clsk1indlem3  44583  grucollcld  44800  inaex  44837  dvgrat  44852  radcnvrat  44854  csbxpgVD  45433  sineq0ALT  45476  trfr  45502  relwf  45507  pwclaxpow  45524  omssaxinf2  45528  islptre  46159  iblspltprt  46511  stoweidlem2  46540  stoweidlem17  46555  stoweidlem21  46559  2reuimp0  47672  2reuimp  47673  afveu  47711  funbrafv  47716  ndmaovass  47764  afv2eu  47796  tz6.12c-afv2  47800  funop1  47841  f1oresf1o2  47849  fvmptrabdm  47851  nltle2tri  47871  2elfz2melfz  47876  fsummsndifre  47938  fsumsplitsndif  47939  fsummmodsndifre  47940  fsummmodsnunz  47941  elsetpreimafvssdm  47956  uniimaelsetpreimafv  47966  imasetpreimafvbijlemfv1  47973  iccpartiltu  47992  iccpartigtl  47993  iccpartleu  47998  iccpartgel  47999  iccpartrn  48000  iccpartiun  48004  icceuelpart  48006  iccpartnel  48008  fargshiftf  48010  fargshiftf1  48011  ichnfb  48035  elsprel  48045  prsprel  48057  sprsymrelfo  48067  paireqne  48081  sbcpr  48091  reupr  48092  fmtnoinf  48109  odz2prm2pw  48136  lighneallem4  48183  lighneal  48184  requad1  48208  requad2  48209  evensumeven  48293  even3prm2  48305  gbowgt5  48348  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  bgoldbnnsum3prm  48390  bgoldbtbndlem2  48392  bgoldbtbndlem4  48394  bgoldbtbnd  48395  dfsclnbgr6  48444  grimco  48475  cycl3grtri  48533  isubgr3stgrlem6  48557  gricgrlic  48604  gpgedgvtx0  48647  gpgprismgr4cycllem3  48683  pgnbgreunbgrlem5  48709  clcllaw  48777  rngccatidALTV  48858  ringccatidALTV  48892  scmsuppss  48957  gsumlsscl  48966  ply1mulgsumlem2  48973  lincvalsc0  49007  linc0scn0  49009  lincdifsn  49010  linc1  49011  lincellss  49012  lincsum  49015  lincscm  49016  lincsumcl  49017  lcoss  49022  lincext3  49042  lindslinindimp2lem4  49047  lindslinindsimp2lem5  49048  lindslinindsimp2  49049  lindsrng01  49054  snlindsntor  49057  lincresunit3lem2  49066  lincresunit3  49067  islindeps2  49069  blengt1fldiv2p1  49179  2arymaptf1  49239  resum2sqorgt0  49295  reorelicc  49296  rrx2plordisom  49309  rrx2linest  49328  rrxsphere  49334  line2ylem  49337  itsclc0xyqsol  49354  itscnhlinecirc02p  49371  mo0sn  49401  thincn0eu  50016