Theorem expcom 414

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ancoms  459  pm3.21  472  sylan  586  animpimp2impd  852  4casesdan  1047  dedlema  1051  dedlemb  1052  sbiedvw  2106  mo4  2570  2moswapv  2633  2moswap  2648  2mosOLD  2654  2eu2  2657  pm2.61ne  3020  nelelne  3034  r19.21be  3233  rspcebdv  3561  2reu2  3837  csbie2df  4378  minel  4401  uneqdifeq  4427  raltpd  4720  ssunsn2  4765  opthprneg  4803  ssuni  4870  uniss2  4879  elpwuni  5041  intss2  5044  disjord  5068  elpw2g  5268  elssabg  5278  axprlem3OLD  5365  axprlem4OLD  5366  axprlem5OLD  5367  axprglem  5372  oteqex  5448  otsndisj  5467  otiunsndisj  5468  epelg  5526  wereu  5621  relop  5799  riinint  5921  sotri3  6087  unixpid  6242  reuop  6251  ordtr2  6362  ordsssuc2  6410  iotan0  6482  funopg  6526  fun  6696  fvmptnf  6965  fvn0ssdmfun  7022  eldmrexrnb  7040  fmptco  7078  fnressn  7108  fressnfv  7110  fprb  7145  fvtp2g  7150  fvtp3g  7151  fconst2g  7154  fntpb  7160  f1dom3el3dif  7220  f1ounsn  7223  isores3  7286  isoselem  7292  oprabv  7423  eloprabga  7472  sorpsscmpl  7684  difex2  7710  ordpwsuc  7762  ordsucun  7772  limuni3  7799  trom  7822  fo1stres  7964  poxp  8075  soxp  8076  xpord3inddlem  8101  soseq  8106  suppimacnv  8121  fsuppeq  8122  funsssuppss  8137  brtpos2  8179  frrlem8  8240  fpr2a  8249  onnseq  8281  smores  8289  smofvon2  8293  tfrlem1  8312  oacl  8467  omcl  8468  oecl  8469  oawordri  8482  oalimcl  8492  oaass  8493  oarec  8494  omwordri  8504  omeulem1  8514  omeulem2  8515  oeordi  8520  oeworde  8526  oeoelem  8531  nnacl  8544  nnmcl  8545  nnecl  8546  nnacom  8550  nnaass  8555  nnmsucr  8558  nnmordi  8564  omabs  8584  cofonr  8607  naddunif  8626  iiner  8733  elpmg  8787  fsetfcdm  8804  fsetprcnex  8806  pmss12g  8814  mapfvd  8824  f1domg  8915  ssdomg  8944  undom  9000  domtriord  9058  ssnnfi  9101  fnfi  9109  enfi  9118  php  9138  sdom1  9157  1sdom2dom  9161  fisseneq  9170  isinf  9172  dif1ennnALT  9184  findcard3  9190  frfi  9192  difinf  9218  imafiOLD  9223  iunfi  9250  fsuppunfi  9298  fsuppres  9303  ffsuppbi  9308  elfi2  9324  marypha1lem  9343  marypha1  9344  oiexg  9447  wemapso2  9465  harword  9475  brwdom  9479  unxpwdom  9501  en3lplem1  9531  inf3lemd  9546  inf3lem5  9551  cantnfval2  9588  cantnfle  9590  cantnflt  9591  cnfcom  9619  tcmin  9658  frr2  9682  r1sdom  9696  rankxplim3  9803  cardidm  9881  cardmin2  9921  infxpenlem  9933  fseqenlem1  9944  numacn  9969  alephordi  9994  iscard3  10013  alephinit  10015  carduniima  10016  iunfictbso  10034  dfac5  10049  dfac12lem3  10066  nnadju  10118  pwsdompw  10123  pwdjudom  10135  cflim2  10183  cfslb2n  10188  cofsmo  10189  cfsmolem  10190  cfcoflem  10192  alephsing  10196  infpssALT  10233  fin23lem34  10266  isf32lem2  10274  isf32lem10  10282  isf32lem12  10284  isfin1-2  10305  hsmexlem4  10349  axcc2lem  10356  domtriomlem  10362  axdc2lem  10368  axdc3lem2  10371  axdc3lem4  10373  axdc4lem  10375  axcclem  10377  ac6num  10399  ac6s  10404  zorn2lem7  10422  ttukeylem5  10433  imadomg  10454  iundom2g  10460  ondomon  10483  ficard  10485  konigthlem  10489  alephreg  10503  pwcfsdom  10504  cfpwsdom  10505  axregndlem1  10523  axregnd  10525  pwfseqlem3  10581  pwxpndom2  10586  pwxpndom  10587  pwdjundom  10588  inawinalem  10610  gchina  10620  wuncval2  10668  tsk0  10684  tskxpss  10693  inatsk  10699  tskuni  10704  gruina  10739  grothac  10751  addclpi  10813  addnidpi  10822  nqereu  10850  mulcanenq  10881  genpnnp  10926  nqpr  10935  prlem934  10954  reclem2pr  10969  suplem1pr  10973  supsrlem  11032  axpre-sup  11090  1re  11142  dedekindle  11308  00id  11319  receu  11793  sup3  12111  infrelb  12139  peano5nni  12175  nnindd  12192  nnaddcl  12195  zrevaddcl  12570  nzadd  12573  zdiv  12597  nneo  12611  zeo2  12614  nn0indd  12624  fzind  12625  fnn0ind  12626  fzindd  12629  uzwo  12859  lbzbi  12884  nn01to3  12889  qrevaddcl  12919  irradd  12921  irrmul  12922  ltsubrp  12978  ltaddrp  12979  xnn0xaddcl  13185  xnn0xadd0  13197  icoshft  13424  fzen  13493  elfzm11  13547  uzsplit  13548  elfzom1elp1fzo  13685  fzoopth  13715  injresinjlem  13743  injresinj  13744  modifeq2int  13893  modsumfzodifsn  13904  om2uzlti  13910  ssnn0fi  13945  fsuppmapnn0fiub0  13953  mptnn0fsuppr  13959  seqcaopr3  13997  seqf1olem2a  14000  seqf1o  14003  ser1const  14018  expadd  14064  expmul  14067  leexp1a  14135  faccl  14243  facdiv  14247  faclbnd  14250  faclbnd4lem4  14256  hasheqf1oi  14311  hashgadd  14337  hashinfxadd  14345  hashunx  14346  hashunsng  14352  elprchashprn2  14356  hashss  14369  hash1snb  14379  hashmap  14395  hashf1lem2  14416  hashf1  14417  seqcoll  14424  hashle2pr  14437  hashdmpropge2  14443  hashge3el3dif  14447  hash1to3  14452  fundmge2nop0  14462  fi1uzind  14467  brfi1indALT  14470  sswrd  14482  swrdnd2  14616  swrdnnn0nd  14617  swrdnd0  14618  swrdwrdsymb  14623  pfxnd0  14649  swrdswrdlem  14664  swrdswrd  14665  wrd2ind  14683  swrdccatin1  14685  swrdccatin2  14689  pfxccatin12lem2  14691  pfxccat3  14694  repsdf2  14738  repswswrd  14744  cshw0  14754  cshwcl  14758  cshwlen  14759  cshf1  14770  swrdco  14797  relexpsucnnl  14990  rtrclreclem3  15020  rtrclreclem4  15021  relexpindlem  15023  rtrclind  15025  shftlem  15028  caubnd  15319  reusq0  15425  rlimcld2  15538  o1dif  15590  climub  15622  climserle  15623  iseraltlem2  15643  sumss  15684  fsumzcl2  15699  fsummsnunz  15714  fsumsplitsnun  15715  fsum2d  15731  modfsummods  15754  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  climcndslem1  15812  climcndslem2  15813  cvgrat  15846  clim2prod  15851  prodfn0  15857  prodfrec  15858  ntrivcvg  15860  prodmo  15899  fprodss  15911  fprodabs  15937  fprodn0  15942  fprod2d  15944  fprodefsum  16058  ruclem8  16202  ruclem9  16203  dvdsmod0  16225  dvds2ln  16256  dvdsaddre2b  16274  dvdslelem  16276  dvdsdivcl  16283  alzdvds  16287  mod2eq1n2dvds  16314  oddnn02np1  16315  nn0o1gt2  16348  nno  16349  sumeven  16354  sumodd  16355  pwp1fsum  16358  ndvdsadd  16377  bitsinv1  16409  sadcadd  16425  sadadd2  16427  saddisjlem  16431  smuval2  16449  smupvallem  16450  smu01lem  16452  smupval  16455  smueqlem  16457  smumullem  16459  gcddiv  16518  rplpwr  16525  nn0seqcvgd  16537  seq1st  16538  alginv  16542  algcvga  16546  algfx  16547  absprodnn  16585  isprm2  16649  isprm3  16650  prmind2  16652  maxprmfct  16677  prmdvdsexp  16683  pcmpt  16861  prmreclem4  16888  vdwmc2  16948  vdwlem10  16959  ramub2  16983  ramcl  16998  prmgaplem5  17024  prmgaplem8  17027  cshwshashlem1  17064  cshwshashlem3  17066  setsn0fun  17141  imasleval  17503  divsfval  17509  mreexexlem4d  17611  isssc  17785  initoeu1  17976  termoeu1  17983  istos  18380  chnfibg  18600  mgmcl  18609  sgrpidmnd  18705  frmdgsum  18828  smndex1mgm  18876  dfgrp3lem  19012  mhmmulg  19089  resghm2b  19207  gsumwrev  19339  elsymgbas  19347  symgextf1  19394  gsmsymgreqlem2  19404  gsmsymgreq  19405  odlem1  19508  odcl2  19538  gexlem1  19552  efgi2  19698  efginvrel2  19700  efgsrel  19707  cyggexb  19872  gsummulglem  19914  gsumzunsnd  19929  gsum2dlem2  19944  telgsums  19966  dmdprd  19973  dprdw  19985  ablfac1eulem  20047  srgpcomp  20197  rnghmmul  20427  nrhmzr  20516  lmodfopnelem1  20895  rmodislmodlem  20926  cnfldmulg  21386  cnfldexp  21387  nzerooringczr  21462  obslbs  21712  mplcoe1  22020  mplcoe3  22021  mplcoe5  22023  cply1mul  22289  coe1fzgsumdlem  22296  gsummoncoe1  22301  pf1ind  22348  evl1gsumdlem  22349  mat1dimcrng  22467  ma1repveval  22561  mulmarep1gsum2  22564  gsummatr01lem3  22647  cramerlem3  22679  decpmatmulsumfsupp  22763  mp2pm2mplem4  22799  pm2mpmhmlem1  22808  fvmptnn04if  22839  cayhamlem1  22856  fctop  22994  mretopd  23082  restopnb  23165  restdis  23168  tgcnp  23243  cncls2  23263  cncls  23264  cnntr  23265  cnsscnp  23269  cmpsub  23390  2ndcsep  23449  1stcelcls  23451  lfinpfin  23514  locfincmp  23516  comppfsc  23522  txcn  23616  txlm  23638  xkohaus  23643  qtopres  23688  haushmphlem  23777  cmphmph  23778  connhmph  23779  reghmph  23783  nrmhmph  23784  ptcmpfi  23803  reghaus  23815  fbssfi  23827  fbun  23830  fbfinnfr  23831  isfildlem  23847  fgcl  23868  cfinfil  23883  supfil  23885  ufinffr  23919  fin1aufil  23922  cnpflf  23991  alexsubALTlem3  24039  alexsubALT  24041  cnextfvval  24055  cnextcn  24057  tmdgsum  24085  tgphaus  24107  tgpt1  24108  mettri  24342  blssexps  24416  blssex  24417  mopni3  24484  metss  24498  psmetutop  24557  dscmet  24562  tngngp3  24646  rectbntr0  24823  metnrmlem1a  24849  fsumcn  24862  lmmbr  25250  caubl  25300  caublcls  25301  bcthlem5  25320  bcth3  25323  ovolunlem1a  25488  ovoliunnul  25499  finiunmbl  25536  voliunlem1  25542  volsuplem  25547  volsup  25548  dyadmax  25590  itgfsum  25819  dvnadd  25921  cpnord  25927  dvnfre  25944  dvmptfsum  25967  dvlip  25985  fta1g  26160  plyco  26231  dgrcolem1  26263  dgrco  26265  dvnply2  26278  plydivex  26288  plyexmo  26304  aannenlem1  26319  aaliou3lem2  26334  dvntaylp  26361  taylthlem1  26363  ulmval  26370  cxpmul2  26678  cxpsqrtth  26719  scvxcvx  26974  jensenlem2  26976  jensen  26977  ppiub  27192  bcmono  27265  bpos1lem  27270  bposlem5  27276  gausslemma2dlem6  27360  lgsquad2lem2  27373  2lgslem3  27392  2lgs  27395  2sqnn  27427  addsqnreup  27431  2sqreultblem  27436  2sqreunnltblem  27439  dchrisumlem1  27477  dchrisum0flb  27498  pntpbnd1  27574  pntlemf  27593  qabvle  27613  qabvexp  27614  ostthlem2  27616  ostth2lem2  27622  ltsval2  27645  ltssolem1  27664  negsprop  28052  mulsuniflem  28166  precsexlem6  28229  precsexlem7  28230  noseqind  28309  om2noseqlt  28316  n0addscl  28361  n0mulscl  28362  expsne0  28453  axeuclidlem  29056  axcontlem12  29069  umgrnloopv  29200  uhgredgrnv  29224  edglnl  29237  numedglnl  29238  usgruspgrb  29277  usgrnloopvALT  29295  usgredg2vlem2  29320  subupgr  29381  nbumgr  29441  uhgrnbgr0nb  29448  nbgr0edglem  29450  edgusgrnbfin  29467  nb3grprlem2  29475  uvtxnbgrvtx  29487  cplgrop  29531  cusgrfi  29552  fusgrmaxsize  29558  fusgrn0degnn0  29593  ewlkprop  29697  uspgr2wlkeq  29739  g0wlk0  29744  wlkreslem  29761  lfgriswlk  29780  upgrwlkdvde  29830  spthonepeq  29845  uhgrwkspth  29848  usgr2trlncl  29853  usgr2trlspth  29854  cyclnumvtx  29893  cyclnspth  29894  crctcshwlkn0lem3  29905  wwlksn  29930  wspthneq1eq2  29953  wwlksm1edg  29974  wwlksnred  29985  wwlksnextfun  29991  wwlksnextinj  29992  wwlksnextproplem3  30004  wspthsnonn0vne  30010  wspn0  30017  rusgrnumwwlk  30071  clwwlkccatlem  30084  umgrclwwlkge2  30086  clwlkclwwlklem2  30095  clwlkclwwlklem3  30096  clwwisshclwws  30110  clwwisshclwwsn  30111  clwwlkn1loopb  30138  wwlksext2clwwlk  30152  wwlksubclwwlk  30153  clwwlknonex2lem2  30203  upgr3v3e3cycl  30275  uhgr3cyclex  30277  upgr4cycl4dv4e  30280  eupth2lem3lem4  30326  eupth2lem3lem7  30329  eupth2  30334  eulerpath  30336  nfrgr2v  30367  frgr3vlem1  30368  3vfriswmgr  30373  1to2vfriswmgr  30374  1to3vfriswmgr  30375  3cyclfrgrrn1  30380  3cyclfrgrrn  30381  3cyclfrgrrn2  30382  4cycl2vnunb  30385  frgrncvvdeqlem2  30395  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  frgrwopreglem4a  30405  frgrwopreglem5lem  30415  frgrwopreglem5ALT  30417  frgrregorufr0  30419  frgr2wwlk1  30424  frgr2wwlkeqm  30426  fusgr2wsp2nb  30429  2wspmdisj  30432  frrusgrord  30436  numclwwlk1lem2f1  30452  numclwlk1  30466  frgrreggt1  30488  friendshipgt3  30493  hlim2  31288  elnlfn  32024  stle0i  32335  hstrbi  32362  spansncv2  32389  h1da  32445  fmptcof2  32756  sgn3da  32933  xreceu  33007  domnprodn0  33363  1arithufdlem3  33636  1arithufdlem4  33637  tpr2rico  34103  hasheuni  34276  ismeas  34390  sseqp1  34586  rrvsum  34645  dstfrvunirn  34666  signstfvc  34765  bnj607  35105  bnj1145  35182  bnj1204  35201  r1filim  35292  fineqvrep  35302  fineqvnttrclselem1  35309  onvf1odlem4  35341  fisshasheq  35350  subgrwlk  35367  subfacp1lem6  35420  cvmlift2lem12  35549  cvmlift3lem4  35557  satfrnmapom  35605  sat1el2xp  35614  satffunlem2  35643  satffun  35644  mrsubvrs  35757  climuzcnv  35906  iprodefisumlem  35975  dfon2lem9  36024  linethru  36388  elhf2  36410  finminlem  36553  fnessref  36592  neibastop2lem  36595  fnemeet2  36602  nndivsub  36692  mh-inf3f1  36776  bj-cbvew  36989  bj-xpnzex  37319  bj-elpwg  37412  bj-epelg  37428  bj-axseprep  37434  mptsnunlem  37707  dissneqlem  37709  topdifinffinlem  37716  iooelexlt  37731  domalom  37773  fvineqsneq  37781  wl-exeq  37912  matunitlindflem1  37990  poimirlem22  38016  poimirlem26  38020  poimirlem28  38022  poimirlem29  38023  poimirlem32  38026  heicant  38029  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  cover2  38089  upixp  38103  sdclem2  38116  fdc  38119  seqpo  38121  metf1o  38129  mettrifi  38131  sstotbnd3  38150  heibor1lem  38183  heiborlem5  38189  heibor  38195  bfplem1  38196  elghomlem2OLD  38260  grpokerinj  38267  isrngo  38271  rngodm1dm2  38306  ispridl2  38412  exlimddvf  38495  lssatle  39514  4atexlemex4  40572  uzindd  42470  evl1gprodd  42609  sn-axprlem3  42712  redvmptabs  42844  sn-sup3d  42989  mzpsubst  43204  jm2.18  43440  wepwsolem  43494  oaabsb  43746  oacl2g  43782  ofoafg  43806  ofoaid1  43810  ofoaid2  43811  naddonnn  43847  iunrelexp0  44153  relexpmulg  44161  cnvtrclfv  44175  clsk1indlem3  44494  grucollcld  44711  inaex  44748  dvgrat  44763  radcnvrat  44765  csbxpgVD  45344  sineq0ALT  45387  trfr  45413  relwf  45418  pwclaxpow  45435  omssaxinf2  45439  islptre  46071  iblspltprt  46423  stoweidlem2  46452  stoweidlem17  46467  stoweidlem21  46471  2reuimp0  47584  2reuimp  47585  afveu  47623  funbrafv  47628  ndmaovass  47676  afv2eu  47708  tz6.12c-afv2  47712  funop1  47753  f1oresf1o2  47761  fvmptrabdm  47763  nltle2tri  47783  2elfz2melfz  47788  fsummsndifre  47850  fsumsplitsndif  47851  fsummmodsndifre  47852  fsummmodsnunz  47853  elsetpreimafvssdm  47868  uniimaelsetpreimafv  47878  imasetpreimafvbijlemfv1  47885  iccpartiltu  47904  iccpartigtl  47905  iccpartleu  47910  iccpartgel  47911  iccpartrn  47912  iccpartiun  47916  icceuelpart  47918  iccpartnel  47920  fargshiftf  47922  fargshiftf1  47923  ichnfb  47947  elsprel  47957  prsprel  47969  sprsymrelfo  47979  paireqne  47993  sbcpr  48003  reupr  48004  fmtnoinf  48021  odz2prm2pw  48048  lighneallem4  48095  lighneal  48096  requad1  48120  requad2  48121  evensumeven  48205  even3prm2  48217  gbowgt5  48260  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbnnsum3prm  48302  bgoldbtbndlem2  48304  bgoldbtbndlem4  48306  bgoldbtbnd  48307  dfsclnbgr6  48356  grimco  48387  cycl3grtri  48445  isubgr3stgrlem6  48469  gricgrlic  48516  gpgedgvtx0  48559  gpgprismgr4cycllem3  48595  pgnbgreunbgrlem5  48621  clcllaw  48689  rngccatidALTV  48770  ringccatidALTV  48804  scmsuppss  48869  gsumlsscl  48878  ply1mulgsumlem2  48885  lincvalsc0  48919  linc0scn0  48921  lincdifsn  48922  linc1  48923  lincellss  48924  lincsum  48927  lincscm  48928  lincsumcl  48929  lcoss  48934  lincext3  48954  lindslinindimp2lem4  48959  lindslinindsimp2lem5  48960  lindslinindsimp2  48961  lindsrng01  48966  snlindsntor  48969  lincresunit3lem2  48978  lincresunit3  48979  islindeps2  48981  blengt1fldiv2p1  49091  2arymaptf1  49151  resum2sqorgt0  49207  reorelicc  49208  rrx2plordisom  49221  rrx2linest  49240  rrxsphere  49246  line2ylem  49249  itsclc0xyqsol  49266  itscnhlinecirc02p  49283  mo0sn  49313  thincn0eu  49928