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

This theorem is referenced by:  ancoms  462  pm3.21  475  sylan  583  animpimp2impd  843  4casesdan  1037  dedlema  1041  dedlemb  1042  sbiedvw  2101  cbval2vOLD  2353  cbval2OLD  2422  mo4  2625  2moswapv  2691  2moswap  2706  2mos  2711  2eu2  2714  pm2.61ne  3072  nelelne  3085  r19.21be  3174  cbvraldva2  3403  cbvrexdva2OLD  3405  rspcebdv  3565  2reu2  3827  csbie2df  4348  minel  4373  uneqdifeq  4396  raltpd  4677  ssunsn2  4720  opthprneg  4755  ssuni  4825  uniss2  4833  elpwuni  4990  intss2  4993  disjord  5018  elssabg  5203  elpw2g  5211  axprlem3  5291  axprlem4  5292  axprlem5  5293  oteqex  5355  otsndisj  5374  otiunsndisj  5375  epelg  5431  wereu  5515  relop  5685  riinint  5804  sotri3  5957  unixpid  6103  reuop  6112  ordtr2  6203  ordsssuc2  6247  iotan0  6314  funopg  6358  fun  6514  tz6.12c  6670  fvmptnf  6767  fvn0ssdmfun  6819  eldmrexrnb  6835  fmptco  6868  fnressn  6897  fressnfv  6899  fprb  6933  fvtp2g  6938  fvtp3g  6939  fconst2g  6942  fntpb  6949  f1dom3el3dif  7005  isores3  7067  isoselem  7073  oprabv  7193  eloprabga  7240  sorpsscmpl  7440  difex2  7462  ordpwsuc  7510  ordsucun  7520  limuni3  7547  ordom  7569  fo1stres  7697  poxp  7805  soxp  7806  suppimacnv  7824  frnsuppeq  7825  funsssuppss  7839  brtpos2  7881  wfrlem12  7949  onnseq  7964  smores  7972  smofvon2  7976  tfrlem1  7995  oacl  8143  omcl  8144  oecl  8145  oawordri  8159  oalimcl  8169  oaass  8170  oarec  8171  omwordri  8181  omeulem1  8191  omeulem2  8192  oeordi  8196  oeworde  8202  oeoelem  8207  nnacl  8220  nnmcl  8221  nnecl  8222  nnacom  8226  nnaass  8231  nnmsucr  8234  nnmordi  8240  omabs  8257  iiner  8352  elpmg  8405  pmss12g  8416  mapfvd  8426  f1domg  8512  ssdomg  8538  domtriord  8647  php  8685  php3  8687  1sdom  8705  fisseneq  8713  isinf  8715  ssnnfi  8721  dif1en  8735  findcard3  8745  frfi  8747  unfi  8769  difinf  8772  fnfi  8780  iunfi  8796  fsuppunfi  8837  fsuppres  8842  frnfsuppbi  8846  elfi2  8862  marypha1lem  8881  marypha1  8882  oiexg  8983  wemapso2  9001  harword  9011  brwdom  9015  unxpwdom  9037  en3lplem1  9059  inf3lemd  9074  inf3lem5  9079  cantnfval2  9116  cantnfle  9118  cantnflt  9119  cnfcom  9147  tcmin  9167  r1sdom  9187  rankxplim3  9294  cardidm  9372  cardmin2  9412  infxpenlem  9424  fseqenlem1  9435  numacn  9460  alephordi  9485  iscard3  9504  alephinit  9506  carduniima  9507  iunfictbso  9525  dfac5  9539  dfac12lem3  9556  nnadju  9608  pwsdompw  9615  pwdjudom  9627  cflim2  9674  cfslb2n  9679  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  alephsing  9687  infpssALT  9724  fin23lem34  9757  isf32lem2  9765  isf32lem10  9773  isf32lem12  9775  isfin1-2  9796  hsmexlem4  9840  axcc2lem  9847  domtriomlem  9853  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ac6num  9890  ac6s  9895  zorn2lem7  9913  ttukeylem5  9924  imadomg  9945  iundom2g  9951  ondomon  9974  ficard  9976  konigthlem  9979  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  axregndlem1  10013  axregnd  10015  pwfseqlem3  10071  pwxpndom2  10076  pwxpndom  10077  pwdjundom  10078  inawinalem  10100  gchina  10110  wuncval2  10158  tsk0  10174  tskxpss  10183  inatsk  10189  tskuni  10194  gruina  10229  grothac  10241  addclpi  10303  addnidpi  10312  nqereu  10340  mulcanenq  10371  genpnnp  10416  nqpr  10425  prlem934  10444  reclem2pr  10459  suplem1pr  10463  supsrlem  10522  axpre-sup  10580  1re  10630  dedekindle  10793  00id  10804  receu  11274  sup3  11585  infrelb  11613  peano5nni  11628  nnindd  11645  nnaddcl  11648  zrevaddcl  12015  nzadd  12018  zdiv  12040  nneo  12054  zeo2  12057  nn0indd  12067  fzind  12068  fnn0ind  12069  uzwo  12299  lbzbi  12324  nn01to3  12329  qrevaddcl  12358  irradd  12360  irrmul  12361  ltsubrp  12413  ltaddrp  12414  xnn0xaddcl  12616  xnn0xadd0  12628  icoshft  12851  fzen  12919  elfzm11  12973  uzsplit  12974  elfzoext  13089  elfzom1elp1fzo  13099  injresinjlem  13152  injresinj  13153  modifeq2int  13296  modsumfzodifsn  13307  om2uzlti  13313  ssnn0fi  13348  fsuppmapnn0fiub0  13356  mptnn0fsuppr  13362  seqcaopr3  13401  seqf1olem2a  13404  seqf1o  13407  ser1const  13422  expadd  13467  expmul  13470  leexp1a  13535  faccl  13639  facdiv  13643  faclbnd  13646  faclbnd4lem4  13652  hasheqf1oi  13708  hashgadd  13734  hashinfxadd  13742  hashunx  13743  hashunsng  13749  elprchashprn2  13753  hashss  13766  hash1snb  13776  hashmap  13792  hashf1lem2  13810  hashf1  13811  seqcoll  13818  hashle2pr  13831  hashdmpropge2  13837  hashge3el3dif  13840  hash1to3  13845  fundmge2nop0  13846  fi1uzind  13851  brfi1indALT  13854  sswrd  13865  swrdnd2  14008  swrdnnn0nd  14009  swrdnd0  14010  swrdwrdsymb  14015  pfxnd0  14041  swrdswrdlem  14057  swrdswrd  14058  wrd2ind  14076  swrdccatin1  14078  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccat3  14087  repsdf2  14131  repswswrd  14137  cshw0  14147  cshwcl  14151  cshwlen  14152  cshf1  14163  swrdco  14190  relexpsucnnl  14381  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  rtrclind  14416  shftlem  14419  caubnd  14710  reusq0  14814  rlimcld2  14927  o1dif  14978  climub  15010  climserle  15011  iseraltlem2  15031  sumss  15073  fsumzcl2  15087  fsummsnunz  15101  fsumsplitsnun  15102  fsum2d  15118  modfsummods  15140  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  climcndslem1  15196  climcndslem2  15197  cvgrat  15231  clim2prod  15236  prodfn0  15242  prodfrec  15243  ntrivcvg  15245  prodmo  15282  fprodss  15294  fprodabs  15320  fprodn0  15325  fprod2d  15327  fprodefsum  15440  ruclem8  15582  ruclem9  15583  dvdsmod0  15605  dvds2ln  15634  dvdsaddre2b  15649  dvdslelem  15651  dvdsdivcl  15658  alzdvds  15662  mod2eq1n2dvds  15688  oddnn02np1  15689  nn0o1gt2  15722  nno  15723  sumeven  15728  sumodd  15729  pwp1fsum  15732  ndvdsadd  15751  bitsinv1  15781  sadcadd  15797  sadadd2  15799  saddisjlem  15803  smuval2  15821  smupvallem  15822  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  gcddiv  15889  gcdmultipleOLD  15890  rplpwr  15897  nn0seqcvgd  15904  seq1st  15905  alginv  15909  algcvga  15913  algfx  15914  absprodnn  15952  isprm2  16016  isprm3  16017  prmind2  16019  maxprmfct  16043  prmdvdsexp  16049  pcmpt  16218  prmreclem4  16245  vdwmc2  16305  vdwlem10  16316  ramub2  16340  ramcl  16355  prmgaplem5  16381  prmgaplem8  16384  cshwshashlem1  16421  cshwshashlem3  16423  setsn0fun  16512  imasleval  16806  divsfval  16812  mreexexlem4d  16910  isssc  17082  initoeu1  17263  termoeu1  17270  istos  17637  mgmcl  17847  sgrpidmnd  17908  frmdgsum  18019  smndex1mgm  18064  dfgrp3lem  18189  mhmmulg  18260  resghm2b  18368  gsumwrev  18486  elsymgbas  18494  symgextf1  18541  gsmsymgreqlem2  18551  gsmsymgreq  18552  odlem1  18655  odcl2  18684  gexlem1  18696  efgi2  18843  efginvrel2  18845  efgsrel  18852  cyggexb  19012  gsummulglem  19054  gsumzunsnd  19069  gsum2dlem2  19084  telgsums  19106  dmdprd  19113  dprdw  19125  ablfac1eulem  19187  srgpcomp  19275  lmodfopnelem1  19663  rmodislmodlem  19694  cnfldmulg  20123  cnfldexp  20124  obslbs  20419  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  cply1mul  20923  coe1fzgsumdlem  20930  gsummoncoe1  20933  pf1ind  20979  evl1gsumdlem  20980  mat1dimcrng  21082  ma1repveval  21176  mulmarep1gsum2  21179  gsummatr01lem3  21262  cramerlem3  21294  decpmatmulsumfsupp  21378  mp2pm2mplem4  21414  pm2mpmhmlem1  21423  fvmptnn04if  21454  cayhamlem1  21471  fctop  21609  mretopd  21697  restopnb  21780  restdis  21783  tgcnp  21858  cncls2  21878  cncls  21879  cnntr  21880  cnsscnp  21884  cmpsub  22005  2ndcsep  22064  1stcelcls  22066  lfinpfin  22129  locfincmp  22131  comppfsc  22137  txcn  22231  txlm  22253  xkohaus  22258  qtopres  22303  haushmphlem  22392  cmphmph  22393  connhmph  22394  reghmph  22398  nrmhmph  22399  ptcmpfi  22418  reghaus  22430  fbssfi  22442  fbun  22445  fbfinnfr  22446  isfildlem  22462  fgcl  22483  cfinfil  22498  supfil  22500  ufinffr  22534  fin1aufil  22537  cnpflf  22606  alexsubALTlem3  22654  alexsubALT  22656  cnextfvval  22670  cnextcn  22672  tmdgsum  22700  tgphaus  22722  tgpt1  22723  mettri  22959  blssexps  23033  blssex  23034  mopni3  23101  metss  23115  psmetutop  23174  dscmet  23179  tngngp3  23262  rectbntr0  23437  metnrmlem1a  23463  fsumcn  23475  lmmbr  23862  caubl  23912  caublcls  23913  bcthlem5  23932  bcth3  23935  ovolunlem1a  24100  ovoliunnul  24111  finiunmbl  24148  voliunlem1  24154  volsuplem  24159  volsup  24160  dyadmax  24202  itgfsum  24430  dvnadd  24532  cpnord  24538  dvnfre  24555  dvmptfsum  24578  dvlip  24596  fta1g  24768  plyco  24838  dgrcolem1  24870  dgrco  24872  dvnply2  24883  plydivex  24893  plyexmo  24909  aannenlem1  24924  aaliou3lem2  24939  dvntaylp  24966  taylthlem1  24968  ulmval  24975  cxpmul2  25280  cxpsqrtth  25320  scvxcvx  25571  jensenlem2  25573  jensen  25574  ppiub  25788  bcmono  25861  bpos1lem  25866  bposlem5  25872  gausslemma2dlem6  25956  lgsquad2lem2  25969  2lgslem3  25988  2lgs  25991  2sqnn  26023  addsqnreup  26027  2sqreultblem  26032  2sqreunnltblem  26035  dchrisumlem1  26073  dchrisum0flb  26094  pntpbnd1  26170  pntlemf  26189  qabvle  26209  qabvexp  26210  ostthlem2  26212  ostth2lem2  26218  axeuclidlem  26756  axcontlem12  26769  umgrnloopv  26899  uhgredgrnv  26923  edglnl  26936  numedglnl  26937  usgruspgrb  26974  usgrnloopvALT  26991  usgredg2vlem2  27016  subupgr  27077  nbumgr  27137  uhgrnbgr0nb  27144  nbgr0vtxlem  27145  edgusgrnbfin  27163  nb3grprlem2  27171  uvtxnbgrvtx  27183  cplgrop  27227  cusgrfi  27248  fusgrmaxsize  27254  fusgrn0degnn0  27289  ewlkprop  27393  uspgr2wlkeq  27435  g0wlk0  27441  wlkreslem  27459  lfgriswlk  27478  upgrwlkdvde  27526  spthonepeq  27541  uhgrwkspth  27544  usgr2trlncl  27549  usgr2trlspth  27550  cyclnspth  27589  crctcshwlkn0lem3  27598  wwlksn  27623  wspthneq1eq2  27646  wwlksm1edg  27667  wwlksnred  27678  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextproplem3  27697  wspthsnonn0vne  27703  wspn0  27710  rusgrnumwwlk  27761  clwwlkccatlem  27774  umgrclwwlkge2  27776  clwlkclwwlklem2  27785  clwlkclwwlklem3  27786  clwwisshclwws  27800  clwwisshclwwsn  27801  clwwlkn1loopb  27828  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  clwwlknonex2lem2  27893  upgr3v3e3cycl  27965  uhgr3cyclex  27967  upgr4cycl4dv4e  27970  eupth2lem3lem4  28016  eupth2lem3lem7  28019  eupth2  28024  eulerpath  28026  nfrgr2v  28057  frgr3vlem1  28058  3vfriswmgr  28063  1to2vfriswmgr  28064  1to3vfriswmgr  28065  3cyclfrgrrn1  28070  3cyclfrgrrn  28071  3cyclfrgrrn2  28072  4cycl2vnunb  28075  frgrncvvdeqlem2  28085  frgrncvvdeqlem8  28091  frgrncvvdeqlem9  28092  frgrwopreglem4a  28095  frgrwopreglem5lem  28105  frgrwopreglem5ALT  28107  frgrregorufr0  28109  frgr2wwlk1  28114  frgr2wwlkeqm  28116  fusgr2wsp2nb  28119  2wspmdisj  28122  frrusgrord  28126  numclwwlk1lem2f1  28142  numclwlk1  28156  frgrreggt1  28178  friendshipgt3  28183  hlim2  28975  elnlfn  29711  stle0i  30022  hstrbi  30049  spansncv2  30076  h1da  30132  fmptcof2  30420  xreceu  30624  tpr2rico  31265  hasheuni  31454  ismeas  31568  sseqp1  31763  rrvsum  31822  dstfrvunirn  31842  sgn3da  31909  signstfvc  31954  bnj607  32298  bnj1145  32375  bnj1204  32394  fisshasheq  32462  subgrwlk  32492  subfacp1lem6  32545  cvmlift2lem12  32674  cvmlift3lem4  32682  satfrnmapom  32730  sat1el2xp  32739  satffunlem2  32768  satffun  32769  mrsubvrs  32882  climuzcnv  33027  iprodefisumlem  33085  dfon2lem9  33149  trpredtr  33182  trpredmintr  33183  dftrpred3g  33185  trpredrec  33190  soseq  33209  frrlem8  33243  fpr2  33253  frr2  33258  sltval2  33276  sltsolem1  33293  linethru  33727  elhf2  33749  finminlem  33779  fnessref  33818  neibastop2lem  33821  fnemeet2  33828  nndivsub  33918  bj-xpnzex  34395  bj-elpwg  34469  bj-epelg  34484  mptsnunlem  34755  dissneqlem  34757  topdifinffinlem  34764  iooelexlt  34779  domalom  34821  fvineqsneq  34829  wl-exeq  34939  wl-ax11-lem3  34984  matunitlindflem1  35053  poimirlem22  35079  poimirlem26  35083  poimirlem28  35085  poimirlem29  35086  poimirlem32  35089  heicant  35092  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  cover2  35152  upixp  35167  sdclem2  35180  fdc  35183  seqpo  35185  metf1o  35193  mettrifi  35195  sstotbnd3  35214  heibor1lem  35247  heiborlem5  35253  heibor  35259  bfplem1  35260  elghomlem2OLD  35324  grpokerinj  35331  isrngo  35335  rngodm1dm2  35370  ispridl2  35476  exlimddvf  35559  lssatle  36311  4atexlemex4  37369  fzindd  39263  uzindd  39264  sn-axprlem3  39401  mzpsubst  39689  jm2.18  39929  wepwsolem  39986  iunrelexp0  40403  relexpmulg  40411  cnvtrclfv  40425  clsk1indlem3  40746  grucollcld  40968  inaex  41005  dvgrat  41016  radcnvrat  41018  csbxpgVD  41600  sineq0ALT  41643  islptre  42261  iblspltprt  42615  stoweidlem2  42644  stoweidlem17  42659  stoweidlem21  42663  2reuimp0  43670  2reuimp  43671  afveu  43709  funbrafv  43714  ndmaovass  43762  afv2eu  43794  tz6.12c-afv2  43798  funop1  43839  f1oresf1o2  43847  fvmptrabdm  43849  nltle2tri  43870  2elfz2melfz  43875  fzoopth  43884  fsummsndifre  43889  fsumsplitsndif  43890  fsummmodsndifre  43891  fsummmodsnunz  43892  elsetpreimafvssdm  43903  uniimaelsetpreimafv  43913  imasetpreimafvbijlemfv1  43920  iccpartiltu  43939  iccpartigtl  43940  iccpartleu  43945  iccpartgel  43946  iccpartrn  43947  iccpartiun  43951  icceuelpart  43953  iccpartnel  43955  fargshiftf  43957  fargshiftf1  43958  ichnfb  43982  elsprel  43992  prsprel  44004  sprsymrelfo  44014  paireqne  44028  sbcpr  44038  reupr  44039  fmtnoinf  44053  odz2prm2pw  44080  lighneallem4  44128  lighneal  44129  requad1  44140  requad2  44141  evensumeven  44225  even3prm2  44237  gbowgt5  44280  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbnnsum3prm  44322  bgoldbtbndlem2  44324  bgoldbtbndlem4  44326  bgoldbtbnd  44327  isomuspgrlem1  44345  clcllaw  44451  nrhmzr  44497  rnghmmul  44524  rngccatidALTV  44613  ringccatidALTV  44676  nzerooringczr  44696  scmsuppss  44774  gsumlsscl  44785  ply1mulgsumlem2  44795  lincvalsc0  44830  linc0scn0  44832  lincdifsn  44833  linc1  44834  lincellss  44835  lincsum  44838  lincscm  44839  lincsumcl  44840  lcoss  44845  lincext3  44865  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  lindsrng01  44877  snlindsntor  44880  lincresunit3lem2  44889  lincresunit3  44890  islindeps2  44892  blengt1fldiv2p1  45007  2arymaptf1  45067  resum2sqorgt0  45123  reorelicc  45124  rrx2plordisom  45137  rrx2linest  45156  rrxsphere  45162  line2ylem  45165  itsclc0xyqsol  45182  itscnhlinecirc02p  45199