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

This theorem is referenced by:  ancoms  459  pm3.21  472  sylan  580  animpimp2impd  844  4casesdan  1040  dedlema  1044  dedlemb  1045  sbiedvw  2096  mo4  2559  2moswapv  2624  2moswap  2639  2mos  2644  2eu2  2647  pm2.61ne  3026  nelelne  3040  r19.21be  3233  cbvraldva2  3321  rspcebdv  3576  2reu2  3857  csbie2df  4405  minel  4430  uneqdifeq  4455  raltpd  4747  ssunsn2  4792  opthprneg  4827  ssuni  4898  uniss2  4907  elpwuni  5070  intss2  5073  disjord  5098  elssabg  5298  elpw2g  5306  axprlem3  5385  axprlem4  5386  axprlem5  5387  oteqex  5462  otsndisj  5481  otiunsndisj  5482  epelg  5543  wereu  5634  relop  5811  riinint  5928  sotri3  6089  unixpid  6241  reuop  6250  ordtr2  6366  ordsssuc2  6413  iotan0  6491  funopg  6540  fun  6709  tz6.12cOLD  6874  fvmptnf  6975  fvn0ssdmfun  7030  eldmrexrnb  7047  fmptco  7080  fnressn  7109  fressnfv  7111  fprb  7148  fvtp2g  7153  fvtp3g  7154  fconst2g  7157  fntpb  7164  f1dom3el3dif  7221  isores3  7285  isoselem  7291  oprabv  7422  eloprabga  7469  eloprabgaOLD  7470  sorpsscmpl  7676  difex2  7699  ordpwsuc  7755  ordsucun  7765  limuni3  7793  trom  7816  fo1stres  7952  poxp  8065  soxp  8066  xpord3inddlem  8091  soseq  8096  suppimacnv  8110  fsuppeq  8111  funsssuppss  8126  brtpos2  8168  frrlem8  8229  fpr2a  8238  wfrlem12OLD  8271  onnseq  8295  smores  8303  smofvon2  8307  tfrlem1  8327  oacl  8486  omcl  8487  oecl  8488  oawordri  8502  oalimcl  8512  oaass  8513  oarec  8514  omwordri  8524  omeulem1  8534  omeulem2  8535  oeordi  8539  oeworde  8545  oeoelem  8550  nnacl  8563  nnmcl  8564  nnecl  8565  nnacom  8569  nnaass  8574  nnmsucr  8577  nnmordi  8583  omabs  8602  cofonr  8625  naddunif  8644  iiner  8735  elpmg  8788  fsetfcdm  8805  fsetprcnex  8807  pmss12g  8814  mapfvd  8824  f1domg  8919  ssdomg  8947  undom  9010  domtriord  9074  ssnnfi  9120  ssnnfiOLD  9121  imafi  9126  fnfi  9132  enfi  9141  php  9161  phpOLD  9173  php3OLD  9175  sdom1  9193  1sdom2dom  9198  1sdomOLD  9200  fisseneq  9208  isinf  9211  isinfOLD  9212  dif1ennnALT  9228  findcard3  9236  findcard3OLD  9237  frfi  9239  unfiOLD  9264  difinf  9267  iunfi  9291  fsuppunfi  9334  fsuppres  9339  ffsuppbi  9343  elfi2  9359  marypha1lem  9378  marypha1  9379  oiexg  9480  wemapso2  9498  harword  9508  brwdom  9512  unxpwdom  9534  en3lplem1  9557  inf3lemd  9572  inf3lem5  9577  cantnfval2  9614  cantnfle  9616  cantnflt  9617  cnfcom  9645  tcmin  9686  frr2  9705  r1sdom  9719  rankxplim3  9826  cardidm  9904  cardmin2  9944  infxpenlem  9958  fseqenlem1  9969  numacn  9994  alephordi  10019  iscard3  10038  alephinit  10040  carduniima  10041  iunfictbso  10059  dfac5  10073  dfac12lem3  10090  nnadju  10142  pwsdompw  10149  pwdjudom  10161  cflim2  10208  cfslb2n  10213  cofsmo  10214  cfsmolem  10215  cfcoflem  10217  alephsing  10221  infpssALT  10258  fin23lem34  10291  isf32lem2  10299  isf32lem10  10307  isf32lem12  10309  isfin1-2  10330  hsmexlem4  10374  axcc2lem  10381  domtriomlem  10387  axdc2lem  10393  axdc3lem2  10396  axdc3lem4  10398  axdc4lem  10400  axcclem  10402  ac6num  10424  ac6s  10429  zorn2lem7  10447  ttukeylem5  10458  imadomg  10479  iundom2g  10485  ondomon  10508  ficard  10510  konigthlem  10513  alephreg  10527  pwcfsdom  10528  cfpwsdom  10529  axregndlem1  10547  axregnd  10549  pwfseqlem3  10605  pwxpndom2  10610  pwxpndom  10611  pwdjundom  10612  inawinalem  10634  gchina  10644  wuncval2  10692  tsk0  10708  tskxpss  10717  inatsk  10723  tskuni  10728  gruina  10763  grothac  10775  addclpi  10837  addnidpi  10846  nqereu  10874  mulcanenq  10905  genpnnp  10950  nqpr  10959  prlem934  10978  reclem2pr  10993  suplem1pr  10997  supsrlem  11056  axpre-sup  11114  1re  11164  dedekindle  11328  00id  11339  receu  11809  sup3  12121  infrelb  12149  peano5nni  12165  nnindd  12182  nnaddcl  12185  zrevaddcl  12557  nzadd  12560  zdiv  12582  nneo  12596  zeo2  12599  nn0indd  12609  fzind  12610  fnn0ind  12611  fzindd  12614  uzwo  12845  lbzbi  12870  nn01to3  12875  qrevaddcl  12905  irradd  12907  irrmul  12908  ltsubrp  12960  ltaddrp  12961  xnn0xaddcl  13164  xnn0xadd0  13176  icoshft  13400  fzen  13468  elfzm11  13522  uzsplit  13523  elfzoext  13639  elfzom1elp1fzo  13649  injresinjlem  13702  injresinj  13703  modifeq2int  13848  modsumfzodifsn  13859  om2uzlti  13865  ssnn0fi  13900  fsuppmapnn0fiub0  13908  mptnn0fsuppr  13914  seqcaopr3  13953  seqf1olem2a  13956  seqf1o  13959  ser1const  13974  expadd  14020  expmul  14023  leexp1a  14090  faccl  14193  facdiv  14197  faclbnd  14200  faclbnd4lem4  14206  hasheqf1oi  14261  hashgadd  14287  hashinfxadd  14295  hashunx  14296  hashunsng  14302  elprchashprn2  14306  hashss  14319  hash1snb  14329  hashmap  14345  hashf1lem2  14367  hashf1  14368  seqcoll  14375  hashle2pr  14388  hashdmpropge2  14394  hashge3el3dif  14397  hash1to3  14402  fundmge2nop0  14403  fi1uzind  14408  brfi1indALT  14411  sswrd  14422  swrdnd2  14555  swrdnnn0nd  14556  swrdnd0  14557  swrdwrdsymb  14562  pfxnd0  14588  swrdswrdlem  14604  swrdswrd  14605  wrd2ind  14623  swrdccatin1  14625  swrdccatin2  14629  pfxccatin12lem2  14631  pfxccat3  14634  repsdf2  14678  repswswrd  14684  cshw0  14694  cshwcl  14698  cshwlen  14699  cshf1  14710  swrdco  14738  relexpsucnnl  14927  rtrclreclem3  14957  rtrclreclem4  14958  relexpindlem  14960  rtrclind  14962  shftlem  14965  caubnd  15255  reusq0  15359  rlimcld2  15472  o1dif  15524  climub  15558  climserle  15559  iseraltlem2  15579  sumss  15620  fsumzcl2  15635  fsummsnunz  15650  fsumsplitsnun  15651  fsum2d  15667  modfsummods  15689  fsumabs  15697  fsumrlim  15707  fsumo1  15708  fsumiun  15717  climcndslem1  15745  climcndslem2  15746  cvgrat  15779  clim2prod  15784  prodfn0  15790  prodfrec  15791  ntrivcvg  15793  prodmo  15830  fprodss  15842  fprodabs  15868  fprodn0  15873  fprod2d  15875  fprodefsum  15988  ruclem8  16130  ruclem9  16131  dvdsmod0  16153  dvds2ln  16182  dvdsaddre2b  16200  dvdslelem  16202  dvdsdivcl  16209  alzdvds  16213  mod2eq1n2dvds  16240  oddnn02np1  16241  nn0o1gt2  16274  nno  16275  sumeven  16280  sumodd  16281  pwp1fsum  16284  ndvdsadd  16303  bitsinv1  16333  sadcadd  16349  sadadd2  16351  saddisjlem  16355  smuval2  16373  smupvallem  16374  smu01lem  16376  smupval  16379  smueqlem  16381  smumullem  16383  gcddiv  16443  rplpwr  16449  nn0seqcvgd  16457  seq1st  16458  alginv  16462  algcvga  16466  algfx  16467  absprodnn  16505  isprm2  16569  isprm3  16570  prmind2  16572  maxprmfct  16596  prmdvdsexp  16602  pcmpt  16775  prmreclem4  16802  vdwmc2  16862  vdwlem10  16873  ramub2  16897  ramcl  16912  prmgaplem5  16938  prmgaplem8  16941  cshwshashlem1  16979  cshwshashlem3  16981  setsn0fun  17056  imasleval  17437  divsfval  17443  mreexexlem4d  17541  isssc  17717  initoeu1  17911  termoeu1  17918  istos  18321  mgmcl  18514  sgrpidmnd  18575  frmdgsum  18686  smndex1mgm  18731  dfgrp3lem  18859  mhmmulg  18931  resghm2b  19040  gsumwrev  19161  elsymgbas  19169  symgextf1  19217  gsmsymgreqlem2  19227  gsmsymgreq  19228  odlem1  19331  odcl2  19361  gexlem1  19375  efgi2  19521  efginvrel2  19523  efgsrel  19530  cyggexb  19690  gsummulglem  19732  gsumzunsnd  19747  gsum2dlem2  19762  telgsums  19784  dmdprd  19791  dprdw  19803  ablfac1eulem  19865  srgpcomp  19963  lmodfopnelem1  20415  rmodislmodlem  20446  cnfldmulg  20866  cnfldexp  20867  obslbs  21173  mplcoe1  21475  mplcoe3  21476  mplcoe5  21478  cply1mul  21702  coe1fzgsumdlem  21709  gsummoncoe1  21712  pf1ind  21758  evl1gsumdlem  21759  mat1dimcrng  21863  ma1repveval  21957  mulmarep1gsum2  21960  gsummatr01lem3  22043  cramerlem3  22075  decpmatmulsumfsupp  22159  mp2pm2mplem4  22195  pm2mpmhmlem1  22204  fvmptnn04if  22235  cayhamlem1  22252  fctop  22391  mretopd  22480  restopnb  22563  restdis  22566  tgcnp  22641  cncls2  22661  cncls  22662  cnntr  22663  cnsscnp  22667  cmpsub  22788  2ndcsep  22847  1stcelcls  22849  lfinpfin  22912  locfincmp  22914  comppfsc  22920  txcn  23014  txlm  23036  xkohaus  23041  qtopres  23086  haushmphlem  23175  cmphmph  23176  connhmph  23177  reghmph  23181  nrmhmph  23182  ptcmpfi  23201  reghaus  23213  fbssfi  23225  fbun  23228  fbfinnfr  23229  isfildlem  23245  fgcl  23266  cfinfil  23281  supfil  23283  ufinffr  23317  fin1aufil  23320  cnpflf  23389  alexsubALTlem3  23437  alexsubALT  23439  cnextfvval  23453  cnextcn  23455  tmdgsum  23483  tgphaus  23505  tgpt1  23506  mettri  23742  blssexps  23816  blssex  23817  mopni3  23887  metss  23901  psmetutop  23960  dscmet  23965  tngngp3  24057  rectbntr0  24232  metnrmlem1a  24258  fsumcn  24270  lmmbr  24659  caubl  24709  caublcls  24710  bcthlem5  24729  bcth3  24732  ovolunlem1a  24897  ovoliunnul  24908  finiunmbl  24945  voliunlem1  24951  volsuplem  24956  volsup  24957  dyadmax  24999  itgfsum  25228  dvnadd  25330  cpnord  25336  dvnfre  25353  dvmptfsum  25376  dvlip  25394  fta1g  25569  plyco  25639  dgrcolem1  25671  dgrco  25673  dvnply2  25684  plydivex  25694  plyexmo  25710  aannenlem1  25725  aaliou3lem2  25740  dvntaylp  25767  taylthlem1  25769  ulmval  25776  cxpmul2  26081  cxpsqrtth  26121  scvxcvx  26372  jensenlem2  26374  jensen  26375  ppiub  26589  bcmono  26662  bpos1lem  26667  bposlem5  26673  gausslemma2dlem6  26757  lgsquad2lem2  26770  2lgslem3  26789  2lgs  26792  2sqnn  26824  addsqnreup  26828  2sqreultblem  26833  2sqreunnltblem  26836  dchrisumlem1  26874  dchrisum0flb  26895  pntpbnd1  26971  pntlemf  26990  qabvle  27010  qabvexp  27011  ostthlem2  27013  ostth2lem2  27019  sltval2  27041  sltsolem1  27060  negsprop  27376  axeuclidlem  27974  axcontlem12  27987  umgrnloopv  28120  uhgredgrnv  28144  edglnl  28157  numedglnl  28158  usgruspgrb  28195  usgrnloopvALT  28212  usgredg2vlem2  28237  subupgr  28298  nbumgr  28358  uhgrnbgr0nb  28365  nbgr0vtxlem  28366  edgusgrnbfin  28384  nb3grprlem2  28392  uvtxnbgrvtx  28404  cplgrop  28448  cusgrfi  28469  fusgrmaxsize  28475  fusgrn0degnn0  28510  ewlkprop  28614  uspgr2wlkeq  28657  g0wlk0  28663  wlkreslem  28680  lfgriswlk  28699  upgrwlkdvde  28748  spthonepeq  28763  uhgrwkspth  28766  usgr2trlncl  28771  usgr2trlspth  28772  cyclnspth  28811  crctcshwlkn0lem3  28820  wwlksn  28845  wspthneq1eq2  28868  wwlksm1edg  28889  wwlksnred  28900  wwlksnextfun  28906  wwlksnextinj  28907  wwlksnextproplem3  28919  wspthsnonn0vne  28925  wspn0  28932  rusgrnumwwlk  28983  clwwlkccatlem  28996  umgrclwwlkge2  28998  clwlkclwwlklem2  29007  clwlkclwwlklem3  29008  clwwisshclwws  29022  clwwisshclwwsn  29023  clwwlkn1loopb  29050  wwlksext2clwwlk  29064  wwlksubclwwlk  29065  clwwlknonex2lem2  29115  upgr3v3e3cycl  29187  uhgr3cyclex  29189  upgr4cycl4dv4e  29192  eupth2lem3lem4  29238  eupth2lem3lem7  29241  eupth2  29246  eulerpath  29248  nfrgr2v  29279  frgr3vlem1  29280  3vfriswmgr  29285  1to2vfriswmgr  29286  1to3vfriswmgr  29287  3cyclfrgrrn1  29292  3cyclfrgrrn  29293  3cyclfrgrrn2  29294  4cycl2vnunb  29297  frgrncvvdeqlem2  29307  frgrncvvdeqlem8  29313  frgrncvvdeqlem9  29314  frgrwopreglem4a  29317  frgrwopreglem5lem  29327  frgrwopreglem5ALT  29329  frgrregorufr0  29331  frgr2wwlk1  29336  frgr2wwlkeqm  29338  fusgr2wsp2nb  29341  2wspmdisj  29344  frrusgrord  29348  numclwwlk1lem2f1  29364  numclwlk1  29378  frgrreggt1  29400  friendshipgt3  29405  hlim2  30197  elnlfn  30933  stle0i  31244  hstrbi  31271  spansncv2  31298  h1da  31354  fmptcof2  31640  xreceu  31848  tpr2rico  32582  hasheuni  32773  ismeas  32887  sseqp1  33084  rrvsum  33143  dstfrvunirn  33163  sgn3da  33230  signstfvc  33275  bnj607  33617  bnj1145  33694  bnj1204  33713  fineqvrep  33785  fisshasheq  33794  subgrwlk  33813  subfacp1lem6  33866  cvmlift2lem12  33995  cvmlift3lem4  34003  satfrnmapom  34051  sat1el2xp  34060  satffunlem2  34089  satffun  34090  mrsubvrs  34203  climuzcnv  34346  iprodefisumlem  34399  dfon2lem9  34452  linethru  34814  elhf2  34836  finminlem  34866  fnessref  34905  neibastop2lem  34908  fnemeet2  34915  nndivsub  35005  bj-xpnzex  35503  bj-elpwg  35596  bj-epelg  35612  mptsnunlem  35882  dissneqlem  35884  topdifinffinlem  35891  iooelexlt  35906  domalom  35948  fvineqsneq  35956  wl-exeq  36066  wl-ax11-lem3  36112  matunitlindflem1  36147  poimirlem22  36173  poimirlem26  36177  poimirlem28  36179  poimirlem29  36180  poimirlem32  36183  heicant  36186  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  cover2  36246  upixp  36261  sdclem2  36274  fdc  36277  seqpo  36279  metf1o  36287  mettrifi  36289  sstotbnd3  36308  heibor1lem  36341  heiborlem5  36347  heibor  36353  bfplem1  36354  elghomlem2OLD  36418  grpokerinj  36425  isrngo  36429  rngodm1dm2  36464  ispridl2  36570  exlimddvf  36653  lssatle  37550  4atexlemex4  38609  uzindd  40507  sn-axprlem3  40710  mzpsubst  41129  jm2.18  41370  wepwsolem  41427  oaabsb  41687  oacl2g  41723  ofoafg  41747  ofoaid1  41751  ofoaid2  41752  naddonnn  41789  iunrelexp0  42096  relexpmulg  42104  cnvtrclfv  42118  clsk1indlem3  42437  grucollcld  42662  inaex  42699  dvgrat  42714  radcnvrat  42716  csbxpgVD  43298  sineq0ALT  43341  islptre  43980  iblspltprt  44334  stoweidlem2  44363  stoweidlem17  44378  stoweidlem21  44382  2reuimp0  45466  2reuimp  45467  afveu  45505  funbrafv  45510  ndmaovass  45558  afv2eu  45590  tz6.12c-afv2  45594  funop1  45635  f1oresf1o2  45643  fvmptrabdm  45645  nltle2tri  45665  2elfz2melfz  45670  fzoopth  45679  fsummsndifre  45684  fsumsplitsndif  45685  fsummmodsndifre  45686  fsummmodsnunz  45687  elsetpreimafvssdm  45698  uniimaelsetpreimafv  45708  imasetpreimafvbijlemfv1  45715  iccpartiltu  45734  iccpartigtl  45735  iccpartleu  45740  iccpartgel  45741  iccpartrn  45742  iccpartiun  45746  icceuelpart  45748  iccpartnel  45750  fargshiftf  45752  fargshiftf1  45753  ichnfb  45777  elsprel  45787  prsprel  45799  sprsymrelfo  45809  paireqne  45823  sbcpr  45833  reupr  45834  fmtnoinf  45848  odz2prm2pw  45875  lighneallem4  45922  lighneal  45923  requad1  45934  requad2  45935  evensumeven  46019  even3prm2  46031  gbowgt5  46074  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  bgoldbnnsum3prm  46116  bgoldbtbndlem2  46118  bgoldbtbndlem4  46120  bgoldbtbnd  46121  isomuspgrlem1  46139  clcllaw  46245  nrhmzr  46291  rnghmmul  46318  rngccatidALTV  46407  ringccatidALTV  46470  nzerooringczr  46490  scmsuppss  46568  gsumlsscl  46579  ply1mulgsumlem2  46588  lincvalsc0  46622  linc0scn0  46624  lincdifsn  46625  linc1  46626  lincellss  46627  lincsum  46630  lincscm  46631  lincsumcl  46632  lcoss  46637  lincext3  46657  lindslinindimp2lem4  46662  lindslinindsimp2lem5  46663  lindslinindsimp2  46664  lindsrng01  46669  snlindsntor  46672  lincresunit3lem2  46681  lincresunit3  46682  islindeps2  46684  blengt1fldiv2p1  46799  2arymaptf1  46859  resum2sqorgt0  46915  reorelicc  46916  rrx2plordisom  46929  rrx2linest  46948  rrxsphere  46954  line2ylem  46957  itsclc0xyqsol  46974  itscnhlinecirc02p  46991  mo0sn  47020  thincn0eu  47172