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  2567  2moswapv  2630  2moswap  2645  2mosOLD  2651  2eu2  2654  pm2.61ne  3018  nelelne  3032  r19.21be  3231  cbvraldva2  3320  rspcebdv  3572  2reu2  3850  csbie2df  4397  minel  4420  uneqdifeq  4447  raltpd  4740  ssunsn2  4785  opthprneg  4823  ssuni  4890  uniss2  4899  elpwuni  5062  intss2  5065  disjord  5089  elpw2g  5280  elssabg  5290  axprlem3OLD  5375  axprlem4OLD  5376  axprlem5OLD  5377  axprglem  5382  oteqex  5456  otsndisj  5475  otiunsndisj  5476  epelg  5533  wereu  5628  relop  5807  riinint  5929  sotri3  6095  unixpid  6250  reuop  6259  ordtr2  6370  ordsssuc2  6418  iotan0  6490  funopg  6534  fun  6704  fvmptnf  6972  fvn0ssdmfun  7028  eldmrexrnb  7046  fmptco  7084  fnressn  7113  fressnfv  7115  fprb  7150  fvtp2g  7155  fvtp3g  7156  fconst2g  7159  fntpb  7165  f1dom3el3dif  7225  f1ounsn  7228  isores3  7291  isoselem  7297  oprabv  7428  eloprabga  7477  sorpsscmpl  7689  difex2  7715  ordpwsuc  7767  ordsucun  7777  limuni3  7804  trom  7827  fo1stres  7969  poxp  8080  soxp  8081  xpord3inddlem  8106  soseq  8111  suppimacnv  8126  fsuppeq  8127  funsssuppss  8142  brtpos2  8184  frrlem8  8245  fpr2a  8254  onnseq  8286  smores  8294  smofvon2  8298  tfrlem1  8317  oacl  8472  omcl  8473  oecl  8474  oawordri  8487  oalimcl  8497  oaass  8498  oarec  8499  omwordri  8509  omeulem1  8519  omeulem2  8520  oeordi  8525  oeworde  8531  oeoelem  8536  nnacl  8549  nnmcl  8550  nnecl  8551  nnacom  8555  nnaass  8560  nnmsucr  8563  nnmordi  8569  omabs  8589  cofonr  8612  naddunif  8631  iiner  8738  elpmg  8792  fsetfcdm  8809  fsetprcnex  8811  pmss12g  8819  mapfvd  8829  f1domg  8920  ssdomg  8949  undom  9005  domtriord  9063  ssnnfi  9106  fnfi  9114  enfi  9123  php  9143  sdom1  9162  1sdom2dom  9166  fisseneq  9175  isinf  9177  dif1ennnALT  9189  findcard3  9195  frfi  9197  difinf  9223  imafiOLD  9228  iunfi  9255  fsuppunfi  9303  fsuppres  9308  ffsuppbi  9313  elfi2  9329  marypha1lem  9348  marypha1  9349  oiexg  9452  wemapso2  9470  harword  9480  brwdom  9484  unxpwdom  9506  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  11309  00id  11320  receu  11794  sup3  12111  infrelb  12139  peano5nni  12160  nnindd  12177  nnaddcl  12180  zrevaddcl  12548  nzadd  12551  zdiv  12574  nneo  12588  zeo2  12591  nn0indd  12601  fzind  12602  fnn0ind  12603  fzindd  12606  uzwo  12836  lbzbi  12861  nn01to3  12866  qrevaddcl  12896  irradd  12898  irrmul  12899  ltsubrp  12955  ltaddrp  12956  xnn0xaddcl  13162  xnn0xadd0  13174  icoshft  13401  fzen  13469  elfzm11  13523  uzsplit  13524  elfzom1elp1fzo  13660  fzoopth  13690  injresinjlem  13718  injresinj  13719  modifeq2int  13868  modsumfzodifsn  13879  om2uzlti  13885  ssnn0fi  13920  fsuppmapnn0fiub0  13928  mptnn0fsuppr  13934  seqcaopr3  13972  seqf1olem2a  13975  seqf1o  13978  ser1const  13993  expadd  14039  expmul  14042  leexp1a  14110  faccl  14218  facdiv  14222  faclbnd  14225  faclbnd4lem4  14231  hasheqf1oi  14286  hashgadd  14312  hashinfxadd  14320  hashunx  14321  hashunsng  14327  elprchashprn2  14331  hashss  14344  hash1snb  14354  hashmap  14370  hashf1lem2  14391  hashf1  14392  seqcoll  14399  hashle2pr  14412  hashdmpropge2  14418  hashge3el3dif  14422  hash1to3  14427  fundmge2nop0  14437  fi1uzind  14442  brfi1indALT  14445  sswrd  14457  swrdnd2  14591  swrdnnn0nd  14592  swrdnd0  14593  swrdwrdsymb  14598  pfxnd0  14624  swrdswrdlem  14639  swrdswrd  14640  wrd2ind  14658  swrdccatin1  14660  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccat3  14669  repsdf2  14713  repswswrd  14719  cshw0  14729  cshwcl  14733  cshwlen  14734  cshf1  14745  swrdco  14772  relexpsucnnl  14965  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  rtrclind  15000  shftlem  15003  caubnd  15294  reusq0  15400  rlimcld2  15513  o1dif  15565  climub  15597  climserle  15598  iseraltlem2  15618  sumss  15659  fsumzcl2  15674  fsummsnunz  15689  fsumsplitsnun  15690  fsum2d  15706  modfsummods  15728  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  climcndslem1  15784  climcndslem2  15785  cvgrat  15818  clim2prod  15823  prodfn0  15829  prodfrec  15830  ntrivcvg  15832  prodmo  15871  fprodss  15883  fprodabs  15909  fprodn0  15914  fprod2d  15916  fprodefsum  16030  ruclem8  16174  ruclem9  16175  dvdsmod0  16197  dvds2ln  16228  dvdsaddre2b  16246  dvdslelem  16248  dvdsdivcl  16255  alzdvds  16259  mod2eq1n2dvds  16286  oddnn02np1  16287  nn0o1gt2  16320  nno  16321  sumeven  16326  sumodd  16327  pwp1fsum  16330  ndvdsadd  16349  bitsinv1  16381  sadcadd  16397  sadadd2  16399  saddisjlem  16403  smuval2  16421  smupvallem  16422  smu01lem  16424  smupval  16427  smueqlem  16429  smumullem  16431  gcddiv  16490  rplpwr  16497  nn0seqcvgd  16509  seq1st  16510  alginv  16514  algcvga  16518  algfx  16519  absprodnn  16557  isprm2  16621  isprm3  16622  prmind2  16624  maxprmfct  16648  prmdvdsexp  16654  pcmpt  16832  prmreclem4  16859  vdwmc2  16919  vdwlem10  16930  ramub2  16954  ramcl  16969  prmgaplem5  16995  prmgaplem8  16998  cshwshashlem1  17035  cshwshashlem3  17037  setsn0fun  17112  imasleval  17474  divsfval  17480  mreexexlem4d  17582  isssc  17756  initoeu1  17947  termoeu1  17954  istos  18351  chnfibg  18571  mgmcl  18580  sgrpidmnd  18676  frmdgsum  18799  smndex1mgm  18844  dfgrp3lem  18980  mhmmulg  19057  resghm2b  19175  gsumwrev  19307  elsymgbas  19315  symgextf1  19362  gsmsymgreqlem2  19372  gsmsymgreq  19373  odlem1  19476  odcl2  19506  gexlem1  19520  efgi2  19666  efginvrel2  19668  efgsrel  19675  cyggexb  19840  gsummulglem  19882  gsumzunsnd  19897  gsum2dlem2  19912  telgsums  19934  dmdprd  19941  dprdw  19953  ablfac1eulem  20015  srgpcomp  20165  rnghmmul  20397  nrhmzr  20482  lmodfopnelem1  20861  rmodislmodlem  20892  cnfldmulg  21370  cnfldexp  21371  nzerooringczr  21447  obslbs  21697  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  cply1mul  22252  coe1fzgsumdlem  22259  gsummoncoe1  22264  pf1ind  22311  evl1gsumdlem  22312  mat1dimcrng  22433  ma1repveval  22527  mulmarep1gsum2  22530  gsummatr01lem3  22613  cramerlem3  22645  decpmatmulsumfsupp  22729  mp2pm2mplem4  22765  pm2mpmhmlem1  22774  fvmptnn04if  22805  cayhamlem1  22822  fctop  22960  mretopd  23048  restopnb  23131  restdis  23134  tgcnp  23209  cncls2  23229  cncls  23230  cnntr  23231  cnsscnp  23235  cmpsub  23356  2ndcsep  23415  1stcelcls  23417  lfinpfin  23480  locfincmp  23482  comppfsc  23488  txcn  23582  txlm  23604  xkohaus  23609  qtopres  23654  haushmphlem  23743  cmphmph  23744  connhmph  23745  reghmph  23749  nrmhmph  23750  ptcmpfi  23769  reghaus  23781  fbssfi  23793  fbun  23796  fbfinnfr  23797  isfildlem  23813  fgcl  23834  cfinfil  23849  supfil  23851  ufinffr  23885  fin1aufil  23888  cnpflf  23957  alexsubALTlem3  24005  alexsubALT  24007  cnextfvval  24021  cnextcn  24023  tmdgsum  24051  tgphaus  24073  tgpt1  24074  mettri  24308  blssexps  24382  blssex  24383  mopni3  24450  metss  24464  psmetutop  24523  dscmet  24528  tngngp3  24612  rectbntr0  24789  metnrmlem1a  24815  fsumcn  24829  lmmbr  25226  caubl  25276  caublcls  25277  bcthlem5  25296  bcth3  25299  ovolunlem1a  25465  ovoliunnul  25476  finiunmbl  25513  voliunlem1  25519  volsuplem  25524  volsup  25525  dyadmax  25567  itgfsum  25796  dvnadd  25899  cpnord  25905  dvnfre  25924  dvmptfsum  25947  dvlip  25966  fta1g  26143  plyco  26214  dgrcolem1  26247  dgrco  26249  dvnply2  26263  plydivex  26273  plyexmo  26289  aannenlem1  26304  aaliou3lem2  26319  dvntaylp  26347  taylthlem1  26349  ulmval  26357  cxpmul2  26666  cxpsqrtth  26707  scvxcvx  26964  jensenlem2  26966  jensen  26967  ppiub  27183  bcmono  27256  bpos1lem  27261  bposlem5  27267  gausslemma2dlem6  27351  lgsquad2lem2  27364  2lgslem3  27383  2lgs  27386  2sqnn  27418  addsqnreup  27422  2sqreultblem  27427  2sqreunnltblem  27430  dchrisumlem1  27468  dchrisum0flb  27489  pntpbnd1  27565  pntlemf  27584  qabvle  27604  qabvexp  27605  ostthlem2  27607  ostth2lem2  27613  ltsval2  27636  ltssolem1  27655  negsprop  28043  mulsuniflem  28157  precsexlem6  28220  precsexlem7  28221  noseqind  28300  om2noseqlt  28307  n0addscl  28352  n0mulscl  28353  expsne0  28444  axeuclidlem  29047  axcontlem12  29060  umgrnloopv  29191  uhgredgrnv  29215  edglnl  29228  numedglnl  29229  usgruspgrb  29268  usgrnloopvALT  29286  usgredg2vlem2  29311  subupgr  29372  nbumgr  29432  uhgrnbgr0nb  29439  nbgr0edglem  29441  edgusgrnbfin  29458  nb3grprlem2  29466  uvtxnbgrvtx  29478  cplgrop  29522  cusgrfi  29544  fusgrmaxsize  29550  fusgrn0degnn0  29585  ewlkprop  29689  uspgr2wlkeq  29731  g0wlk0  29736  wlkreslem  29753  lfgriswlk  29772  upgrwlkdvde  29822  spthonepeq  29837  uhgrwkspth  29840  usgr2trlncl  29845  usgr2trlspth  29846  cyclnumvtx  29885  cyclnspth  29886  crctcshwlkn0lem3  29897  wwlksn  29922  wspthneq1eq2  29945  wwlksm1edg  29966  wwlksnred  29977  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextproplem3  29996  wspthsnonn0vne  30002  wspn0  30009  rusgrnumwwlk  30063  clwwlkccatlem  30076  umgrclwwlkge2  30078  clwlkclwwlklem2  30087  clwlkclwwlklem3  30088  clwwisshclwws  30102  clwwisshclwwsn  30103  clwwlkn1loopb  30130  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  clwwlknonex2lem2  30195  upgr3v3e3cycl  30267  uhgr3cyclex  30269  upgr4cycl4dv4e  30272  eupth2lem3lem4  30318  eupth2lem3lem7  30321  eupth2  30326  eulerpath  30328  nfrgr2v  30359  frgr3vlem1  30360  3vfriswmgr  30365  1to2vfriswmgr  30366  1to3vfriswmgr  30367  3cyclfrgrrn1  30372  3cyclfrgrrn  30373  3cyclfrgrrn2  30374  4cycl2vnunb  30377  frgrncvvdeqlem2  30387  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  frgrwopreglem4a  30397  frgrwopreglem5lem  30407  frgrwopreglem5ALT  30409  frgrregorufr0  30411  frgr2wwlk1  30416  frgr2wwlkeqm  30418  fusgr2wsp2nb  30421  2wspmdisj  30424  frrusgrord  30428  numclwwlk1lem2f1  30444  numclwlk1  30458  frgrreggt1  30480  friendshipgt3  30485  hlim2  31279  elnlfn  32015  stle0i  32326  hstrbi  32353  spansncv2  32380  h1da  32436  fmptcof2  32746  sgn3da  32925  xreceu  33013  domnprodn0  33368  1arithufdlem3  33638  1arithufdlem4  33639  tpr2rico  34089  hasheuni  34262  ismeas  34376  sseqp1  34572  rrvsum  34631  dstfrvunirn  34652  signstfvc  34751  bnj607  35091  bnj1145  35168  bnj1204  35187  r1filim  35279  fineqvrep  35289  fineqvnttrclselem1  35296  onvf1odlem4  35319  fisshasheq  35328  subgrwlk  35345  subfacp1lem6  35398  cvmlift2lem12  35527  cvmlift3lem4  35535  satfrnmapom  35583  sat1el2xp  35592  satffunlem2  35621  satffun  35622  mrsubvrs  35735  climuzcnv  35884  iprodefisumlem  35953  dfon2lem9  36002  linethru  36366  elhf2  36388  finminlem  36531  fnessref  36570  neibastop2lem  36573  fnemeet2  36580  nndivsub  36670  bj-cbvew  36879  bj-xpnzex  37201  bj-elpwg  37294  bj-epelg  37310  bj-axseprep  37316  mptsnunlem  37587  dissneqlem  37589  topdifinffinlem  37596  iooelexlt  37611  domalom  37653  fvineqsneq  37661  wl-exeq  37783  matunitlindflem1  37861  poimirlem22  37887  poimirlem26  37891  poimirlem28  37893  poimirlem29  37894  poimirlem32  37897  heicant  37900  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  cover2  37960  upixp  37974  sdclem2  37987  fdc  37990  seqpo  37992  metf1o  38000  mettrifi  38002  sstotbnd3  38021  heibor1lem  38054  heiborlem5  38060  heibor  38066  bfplem1  38067  elghomlem2OLD  38131  grpokerinj  38138  isrngo  38142  rngodm1dm2  38177  ispridl2  38283  exlimddvf  38366  lssatle  39385  4atexlemex4  40443  uzindd  42341  evl1gprodd  42481  sn-axprlem3  42584  redvmptabs  42724  sn-sup3d  42856  mzpsubst  43099  jm2.18  43339  wepwsolem  43393  oaabsb  43645  oacl2g  43681  ofoafg  43705  ofoaid1  43709  ofoaid2  43710  naddonnn  43746  iunrelexp0  44052  relexpmulg  44060  cnvtrclfv  44074  clsk1indlem3  44393  grucollcld  44610  inaex  44647  dvgrat  44662  radcnvrat  44664  csbxpgVD  45243  sineq0ALT  45286  trfr  45312  relwf  45317  pwclaxpow  45334  omssaxinf2  45338  islptre  45973  iblspltprt  46325  stoweidlem2  46354  stoweidlem17  46369  stoweidlem21  46373  2reuimp0  47468  2reuimp  47469  afveu  47507  funbrafv  47512  ndmaovass  47560  afv2eu  47592  tz6.12c-afv2  47596  funop1  47637  f1oresf1o2  47645  fvmptrabdm  47647  nltle2tri  47667  2elfz2melfz  47672  fsummsndifre  47726  fsumsplitsndif  47727  fsummmodsndifre  47728  fsummmodsnunz  47729  elsetpreimafvssdm  47740  uniimaelsetpreimafv  47750  imasetpreimafvbijlemfv1  47757  iccpartiltu  47776  iccpartigtl  47777  iccpartleu  47782  iccpartgel  47783  iccpartrn  47784  iccpartiun  47788  icceuelpart  47790  iccpartnel  47792  fargshiftf  47794  fargshiftf1  47795  ichnfb  47819  elsprel  47829  prsprel  47841  sprsymrelfo  47851  paireqne  47865  sbcpr  47875  reupr  47876  fmtnoinf  47890  odz2prm2pw  47917  lighneallem4  47964  lighneal  47965  requad1  47976  requad2  47977  evensumeven  48061  even3prm2  48073  gbowgt5  48116  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  bgoldbnnsum3prm  48158  bgoldbtbndlem2  48160  bgoldbtbndlem4  48162  bgoldbtbnd  48163  dfsclnbgr6  48212  grimco  48243  cycl3grtri  48301  isubgr3stgrlem6  48325  gricgrlic  48372  gpgedgvtx0  48415  gpgprismgr4cycllem3  48451  pgnbgreunbgrlem5  48477  clcllaw  48545  rngccatidALTV  48626  ringccatidALTV  48660  scmsuppss  48725  gsumlsscl  48734  ply1mulgsumlem2  48741  lincvalsc0  48775  linc0scn0  48777  lincdifsn  48778  linc1  48779  lincellss  48780  lincsum  48783  lincscm  48784  lincsumcl  48785  lcoss  48790  lincext3  48810  lindslinindimp2lem4  48815  lindslinindsimp2lem5  48816  lindslinindsimp2  48817  lindsrng01  48822  snlindsntor  48825  lincresunit3lem2  48834  lincresunit3  48835  islindeps2  48837  blengt1fldiv2p1  48947  2arymaptf1  49007  resum2sqorgt0  49063  reorelicc  49064  rrx2plordisom  49077  rrx2linest  49096  rrxsphere  49102  line2ylem  49105  itsclc0xyqsol  49122  itscnhlinecirc02p  49139  mo0sn  49169  thincn0eu  49784