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  843  4casesdan  1039  dedlema  1043  dedlemb  1044  sbiedvw  2096  cbval2vOLD  2341  mo4  2566  2moswapv  2631  2moswap  2646  2mos  2651  2eu2  2654  pm2.61ne  3030  nelelne  3043  r19.21be  3134  cbvraldva2  3389  rspcebdv  3552  2reu2  3830  csbie2df  4374  minel  4399  uneqdifeq  4423  raltpd  4717  ssunsn2  4760  opthprneg  4795  ssuni  4866  uniss2  4874  elpwuni  5033  intss2  5036  disjord  5061  elssabg  5258  elpw2g  5266  axprlem3  5346  axprlem4  5347  axprlem5  5348  oteqex  5412  otsndisj  5431  otiunsndisj  5432  epelg  5491  wereu  5580  relop  5752  riinint  5870  sotri3  6028  unixpid  6180  reuop  6189  ordtr2  6303  ordsssuc2  6347  iotan0  6416  funopg  6460  fun  6628  tz6.12c  6791  fvmptnf  6889  fvn0ssdmfun  6944  eldmrexrnb  6960  fmptco  6993  fnressn  7022  fressnfv  7024  fprb  7061  fvtp2g  7066  fvtp3g  7067  fconst2g  7070  fntpb  7077  f1dom3el3dif  7134  isores3  7198  isoselem  7204  oprabv  7325  eloprabga  7372  eloprabgaOLD  7373  sorpsscmpl  7577  difex2  7600  ordpwsuc  7652  ordsucun  7662  limuni3  7689  trom  7711  fo1stres  7846  poxp  7956  soxp  7957  suppimacnv  7977  frnsuppeq  7978  funsssuppss  7993  brtpos2  8035  frrlem8  8096  fpr2a  8105  wfrlem12OLD  8138  onnseq  8162  smores  8170  smofvon2  8174  tfrlem1  8194  oacl  8352  omcl  8353  oecl  8354  oawordri  8368  oalimcl  8378  oaass  8379  oarec  8380  omwordri  8390  omeulem1  8400  omeulem2  8401  oeordi  8405  oeworde  8411  oeoelem  8416  nnacl  8429  nnmcl  8430  nnecl  8431  nnacom  8435  nnaass  8440  nnmsucr  8443  nnmordi  8449  omabs  8468  iiner  8565  elpmg  8618  fsetfcdm  8635  fsetprcnex  8637  pmss12g  8644  mapfvd  8654  f1domg  8747  ssdomg  8773  undom  8833  domtriord  8897  ssnnfi  8939  ssnnfiOLD  8940  imafi  8945  fnfi  8951  enfi  8960  php  8980  phpOLD  8992  php3OLD  8994  1sdom  9012  fisseneq  9021  isinf  9023  dif1enALT  9037  findcard3  9044  frfi  9046  unfiOLD  9068  difinf  9071  iunfi  9094  fsuppunfi  9135  fsuppres  9140  frnfsuppbi  9144  elfi2  9160  marypha1lem  9179  marypha1  9180  oiexg  9281  wemapso2  9299  harword  9309  brwdom  9313  unxpwdom  9335  en3lplem1  9357  inf3lemd  9372  inf3lem5  9377  cantnfval2  9414  cantnfle  9416  cantnflt  9417  cnfcom  9445  trpredtr  9486  trpredmintr  9487  dftrpred3g  9490  trpredrec  9493  tcmin  9508  frr2  9528  r1sdom  9542  rankxplim3  9649  cardidm  9727  cardmin2  9767  infxpenlem  9779  fseqenlem1  9790  numacn  9815  alephordi  9840  iscard3  9859  alephinit  9861  carduniima  9862  iunfictbso  9880  dfac5  9894  dfac12lem3  9911  nnadju  9963  pwsdompw  9970  pwdjudom  9982  cflim2  10029  cfslb2n  10034  cofsmo  10035  cfsmolem  10036  cfcoflem  10038  alephsing  10042  infpssALT  10079  fin23lem34  10112  isf32lem2  10120  isf32lem10  10128  isf32lem12  10130  isfin1-2  10151  hsmexlem4  10195  axcc2lem  10202  domtriomlem  10208  axdc2lem  10214  axdc3lem2  10217  axdc3lem4  10219  axdc4lem  10221  axcclem  10223  ac6num  10245  ac6s  10250  zorn2lem7  10268  ttukeylem5  10279  imadomg  10300  iundom2g  10306  ondomon  10329  ficard  10331  konigthlem  10334  alephreg  10348  pwcfsdom  10349  cfpwsdom  10350  axregndlem1  10368  axregnd  10370  pwfseqlem3  10426  pwxpndom2  10431  pwxpndom  10432  pwdjundom  10433  inawinalem  10455  gchina  10465  wuncval2  10513  tsk0  10529  tskxpss  10538  inatsk  10544  tskuni  10549  gruina  10584  grothac  10596  addclpi  10658  addnidpi  10667  nqereu  10695  mulcanenq  10726  genpnnp  10771  nqpr  10780  prlem934  10799  reclem2pr  10814  suplem1pr  10818  supsrlem  10877  axpre-sup  10935  1re  10985  dedekindle  11149  00id  11160  receu  11630  sup3  11942  infrelb  11970  peano5nni  11986  nnindd  12003  nnaddcl  12006  zrevaddcl  12375  nzadd  12378  zdiv  12400  nneo  12414  zeo2  12417  nn0indd  12427  fzind  12428  fnn0ind  12429  fzindd  12432  uzwo  12661  lbzbi  12686  nn01to3  12691  qrevaddcl  12721  irradd  12723  irrmul  12724  ltsubrp  12776  ltaddrp  12777  xnn0xaddcl  12979  xnn0xadd0  12991  icoshft  13215  fzen  13283  elfzm11  13337  uzsplit  13338  elfzoext  13454  elfzom1elp1fzo  13464  injresinjlem  13517  injresinj  13518  modifeq2int  13663  modsumfzodifsn  13674  om2uzlti  13680  ssnn0fi  13715  fsuppmapnn0fiub0  13723  mptnn0fsuppr  13729  seqcaopr3  13768  seqf1olem2a  13771  seqf1o  13774  ser1const  13789  expadd  13835  expmul  13838  leexp1a  13903  faccl  14007  facdiv  14011  faclbnd  14014  faclbnd4lem4  14020  hasheqf1oi  14076  hashgadd  14102  hashinfxadd  14110  hashunx  14111  hashunsng  14117  elprchashprn2  14121  hashss  14134  hash1snb  14144  hashmap  14160  hashf1lem2  14180  hashf1  14181  seqcoll  14188  hashle2pr  14201  hashdmpropge2  14207  hashge3el3dif  14210  hash1to3  14215  fundmge2nop0  14216  fi1uzind  14221  brfi1indALT  14224  sswrd  14235  swrdnd2  14378  swrdnnn0nd  14379  swrdnd0  14380  swrdwrdsymb  14385  pfxnd0  14411  swrdswrdlem  14427  swrdswrd  14428  wrd2ind  14446  swrdccatin1  14448  swrdccatin2  14452  pfxccatin12lem2  14454  pfxccat3  14457  repsdf2  14501  repswswrd  14507  cshw0  14517  cshwcl  14521  cshwlen  14522  cshf1  14533  swrdco  14560  relexpsucnnl  14751  rtrclreclem3  14781  rtrclreclem4  14782  relexpindlem  14784  rtrclind  14786  shftlem  14789  caubnd  15080  reusq0  15184  rlimcld2  15297  o1dif  15349  climub  15383  climserle  15384  iseraltlem2  15404  sumss  15446  fsumzcl2  15461  fsummsnunz  15476  fsumsplitsnun  15477  fsum2d  15493  modfsummods  15515  fsumabs  15523  fsumrlim  15533  fsumo1  15534  fsumiun  15543  climcndslem1  15571  climcndslem2  15572  cvgrat  15605  clim2prod  15610  prodfn0  15616  prodfrec  15617  ntrivcvg  15619  prodmo  15656  fprodss  15668  fprodabs  15694  fprodn0  15699  fprod2d  15701  fprodefsum  15814  ruclem8  15956  ruclem9  15957  dvdsmod0  15979  dvds2ln  16008  dvdsaddre2b  16026  dvdslelem  16028  dvdsdivcl  16035  alzdvds  16039  mod2eq1n2dvds  16066  oddnn02np1  16067  nn0o1gt2  16100  nno  16101  sumeven  16106  sumodd  16107  pwp1fsum  16110  ndvdsadd  16129  bitsinv1  16159  sadcadd  16175  sadadd2  16177  saddisjlem  16181  smuval2  16199  smupvallem  16200  smu01lem  16202  smupval  16205  smueqlem  16207  smumullem  16209  gcddiv  16269  gcdmultipleOLD  16270  rplpwr  16277  nn0seqcvgd  16285  seq1st  16286  alginv  16290  algcvga  16294  algfx  16295  absprodnn  16333  isprm2  16397  isprm3  16398  prmind2  16400  maxprmfct  16424  prmdvdsexp  16430  pcmpt  16603  prmreclem4  16630  vdwmc2  16690  vdwlem10  16701  ramub2  16725  ramcl  16740  prmgaplem5  16766  prmgaplem8  16769  cshwshashlem1  16807  cshwshashlem3  16809  setsn0fun  16884  imasleval  17262  divsfval  17268  mreexexlem4d  17366  isssc  17542  initoeu1  17736  termoeu1  17743  istos  18146  mgmcl  18339  sgrpidmnd  18400  frmdgsum  18511  smndex1mgm  18556  dfgrp3lem  18683  mhmmulg  18754  resghm2b  18862  gsumwrev  18983  elsymgbas  18991  symgextf1  19039  gsmsymgreqlem2  19049  gsmsymgreq  19050  odlem1  19153  odcl2  19182  gexlem1  19194  efgi2  19341  efginvrel2  19343  efgsrel  19350  cyggexb  19510  gsummulglem  19552  gsumzunsnd  19567  gsum2dlem2  19582  telgsums  19604  dmdprd  19611  dprdw  19623  ablfac1eulem  19685  srgpcomp  19778  lmodfopnelem1  20169  rmodislmodlem  20200  cnfldmulg  20640  cnfldexp  20641  obslbs  20947  mplcoe1  21248  mplcoe3  21249  mplcoe5  21251  cply1mul  21475  coe1fzgsumdlem  21482  gsummoncoe1  21485  pf1ind  21531  evl1gsumdlem  21532  mat1dimcrng  21636  ma1repveval  21730  mulmarep1gsum2  21733  gsummatr01lem3  21816  cramerlem3  21848  decpmatmulsumfsupp  21932  mp2pm2mplem4  21968  pm2mpmhmlem1  21977  fvmptnn04if  22008  cayhamlem1  22025  fctop  22164  mretopd  22253  restopnb  22336  restdis  22339  tgcnp  22414  cncls2  22434  cncls  22435  cnntr  22436  cnsscnp  22440  cmpsub  22561  2ndcsep  22620  1stcelcls  22622  lfinpfin  22685  locfincmp  22687  comppfsc  22693  txcn  22787  txlm  22809  xkohaus  22814  qtopres  22859  haushmphlem  22948  cmphmph  22949  connhmph  22950  reghmph  22954  nrmhmph  22955  ptcmpfi  22974  reghaus  22986  fbssfi  22998  fbun  23001  fbfinnfr  23002  isfildlem  23018  fgcl  23039  cfinfil  23054  supfil  23056  ufinffr  23090  fin1aufil  23093  cnpflf  23162  alexsubALTlem3  23210  alexsubALT  23212  cnextfvval  23226  cnextcn  23228  tmdgsum  23256  tgphaus  23278  tgpt1  23279  mettri  23515  blssexps  23589  blssex  23590  mopni3  23660  metss  23674  psmetutop  23733  dscmet  23738  tngngp3  23830  rectbntr0  24005  metnrmlem1a  24031  fsumcn  24043  lmmbr  24432  caubl  24482  caublcls  24483  bcthlem5  24502  bcth3  24505  ovolunlem1a  24670  ovoliunnul  24681  finiunmbl  24718  voliunlem1  24724  volsuplem  24729  volsup  24730  dyadmax  24772  itgfsum  25001  dvnadd  25103  cpnord  25109  dvnfre  25126  dvmptfsum  25149  dvlip  25167  fta1g  25342  plyco  25412  dgrcolem1  25444  dgrco  25446  dvnply2  25457  plydivex  25467  plyexmo  25483  aannenlem1  25498  aaliou3lem2  25513  dvntaylp  25540  taylthlem1  25542  ulmval  25549  cxpmul2  25854  cxpsqrtth  25894  scvxcvx  26145  jensenlem2  26147  jensen  26148  ppiub  26362  bcmono  26435  bpos1lem  26440  bposlem5  26446  gausslemma2dlem6  26530  lgsquad2lem2  26543  2lgslem3  26562  2lgs  26565  2sqnn  26597  addsqnreup  26601  2sqreultblem  26606  2sqreunnltblem  26609  dchrisumlem1  26647  dchrisum0flb  26668  pntpbnd1  26744  pntlemf  26763  qabvle  26783  qabvexp  26784  ostthlem2  26786  ostth2lem2  26792  axeuclidlem  27340  axcontlem12  27353  umgrnloopv  27486  uhgredgrnv  27510  edglnl  27523  numedglnl  27524  usgruspgrb  27561  usgrnloopvALT  27578  usgredg2vlem2  27603  subupgr  27664  nbumgr  27724  uhgrnbgr0nb  27731  nbgr0vtxlem  27732  edgusgrnbfin  27750  nb3grprlem2  27758  uvtxnbgrvtx  27770  cplgrop  27814  cusgrfi  27835  fusgrmaxsize  27841  fusgrn0degnn0  27876  ewlkprop  27980  uspgr2wlkeq  28022  g0wlk0  28028  wlkreslem  28046  lfgriswlk  28065  upgrwlkdvde  28113  spthonepeq  28128  uhgrwkspth  28131  usgr2trlncl  28136  usgr2trlspth  28137  cyclnspth  28176  crctcshwlkn0lem3  28185  wwlksn  28210  wspthneq1eq2  28233  wwlksm1edg  28254  wwlksnred  28265  wwlksnextfun  28271  wwlksnextinj  28272  wwlksnextproplem3  28284  wspthsnonn0vne  28290  wspn0  28297  rusgrnumwwlk  28348  clwwlkccatlem  28361  umgrclwwlkge2  28363  clwlkclwwlklem2  28372  clwlkclwwlklem3  28373  clwwisshclwws  28387  clwwisshclwwsn  28388  clwwlkn1loopb  28415  wwlksext2clwwlk  28429  wwlksubclwwlk  28430  clwwlknonex2lem2  28480  upgr3v3e3cycl  28552  uhgr3cyclex  28554  upgr4cycl4dv4e  28557  eupth2lem3lem4  28603  eupth2lem3lem7  28606  eupth2  28611  eulerpath  28613  nfrgr2v  28644  frgr3vlem1  28645  3vfriswmgr  28650  1to2vfriswmgr  28651  1to3vfriswmgr  28652  3cyclfrgrrn1  28657  3cyclfrgrrn  28658  3cyclfrgrrn2  28659  4cycl2vnunb  28662  frgrncvvdeqlem2  28672  frgrncvvdeqlem8  28678  frgrncvvdeqlem9  28679  frgrwopreglem4a  28682  frgrwopreglem5lem  28692  frgrwopreglem5ALT  28694  frgrregorufr0  28696  frgr2wwlk1  28701  frgr2wwlkeqm  28703  fusgr2wsp2nb  28706  2wspmdisj  28709  frrusgrord  28713  numclwwlk1lem2f1  28729  numclwlk1  28743  frgrreggt1  28765  friendshipgt3  28770  hlim2  29562  elnlfn  30298  stle0i  30609  hstrbi  30636  spansncv2  30663  h1da  30719  fmptcof2  31002  xreceu  31204  tpr2rico  31870  hasheuni  32061  ismeas  32175  sseqp1  32370  rrvsum  32429  dstfrvunirn  32449  sgn3da  32516  signstfvc  32561  bnj607  32904  bnj1145  32981  bnj1204  33000  fineqvrep  33072  fisshasheq  33081  subgrwlk  33102  subfacp1lem6  33155  cvmlift2lem12  33284  cvmlift3lem4  33292  satfrnmapom  33340  sat1el2xp  33349  satffunlem2  33378  satffun  33379  mrsubvrs  33492  climuzcnv  33637  iprodefisumlem  33714  dfon2lem9  33775  soseq  33811  sltval2  33867  sltsolem1  33886  linethru  34463  elhf2  34485  finminlem  34515  fnessref  34554  neibastop2lem  34557  fnemeet2  34564  nndivsub  34654  bj-xpnzex  35157  bj-elpwg  35233  bj-epelg  35247  mptsnunlem  35517  dissneqlem  35519  topdifinffinlem  35526  iooelexlt  35541  domalom  35583  fvineqsneq  35591  wl-exeq  35701  wl-ax11-lem3  35746  matunitlindflem1  35781  poimirlem22  35807  poimirlem26  35811  poimirlem28  35813  poimirlem29  35814  poimirlem32  35817  heicant  35820  ovoliunnfl  35827  voliunnfl  35829  volsupnfl  35830  cover2  35880  upixp  35895  sdclem2  35908  fdc  35911  seqpo  35913  metf1o  35921  mettrifi  35923  sstotbnd3  35942  heibor1lem  35975  heiborlem5  35981  heibor  35987  bfplem1  35988  elghomlem2OLD  36052  grpokerinj  36059  isrngo  36063  rngodm1dm2  36098  ispridl2  36204  exlimddvf  36287  lssatle  37037  4atexlemex4  38095  uzindd  39993  sn-axprlem3  40194  mzpsubst  40578  jm2.18  40818  wepwsolem  40875  iunrelexp0  41291  relexpmulg  41299  cnvtrclfv  41313  clsk1indlem3  41634  grucollcld  41859  inaex  41896  dvgrat  41911  radcnvrat  41913  csbxpgVD  42495  sineq0ALT  42538  islptre  43141  iblspltprt  43495  stoweidlem2  43524  stoweidlem17  43539  stoweidlem21  43543  2reuimp0  44584  2reuimp  44585  afveu  44623  funbrafv  44628  ndmaovass  44676  afv2eu  44708  tz6.12c-afv2  44712  funop1  44753  f1oresf1o2  44761  fvmptrabdm  44763  nltle2tri  44783  2elfz2melfz  44788  fzoopth  44797  fsummsndifre  44802  fsumsplitsndif  44803  fsummmodsndifre  44804  fsummmodsnunz  44805  elsetpreimafvssdm  44816  uniimaelsetpreimafv  44826  imasetpreimafvbijlemfv1  44833  iccpartiltu  44852  iccpartigtl  44853  iccpartleu  44858  iccpartgel  44859  iccpartrn  44860  iccpartiun  44864  icceuelpart  44866  iccpartnel  44868  fargshiftf  44870  fargshiftf1  44871  ichnfb  44895  elsprel  44905  prsprel  44917  sprsymrelfo  44927  paireqne  44941  sbcpr  44951  reupr  44952  fmtnoinf  44966  odz2prm2pw  44993  lighneallem4  45040  lighneal  45041  requad1  45052  requad2  45053  evensumeven  45137  even3prm2  45149  gbowgt5  45192  nnsum4primeseven  45230  nnsum4primesevenALTV  45231  bgoldbnnsum3prm  45234  bgoldbtbndlem2  45236  bgoldbtbndlem4  45238  bgoldbtbnd  45239  isomuspgrlem1  45257  clcllaw  45363  nrhmzr  45409  rnghmmul  45436  rngccatidALTV  45525  ringccatidALTV  45588  nzerooringczr  45608  scmsuppss  45686  gsumlsscl  45697  ply1mulgsumlem2  45706  lincvalsc0  45740  linc0scn0  45742  lincdifsn  45743  linc1  45744  lincellss  45745  lincsum  45748  lincscm  45749  lincsumcl  45750  lcoss  45755  lincext3  45775  lindslinindimp2lem4  45780  lindslinindsimp2lem5  45781  lindslinindsimp2  45782  lindsrng01  45787  snlindsntor  45790  lincresunit3lem2  45799  lincresunit3  45800  islindeps2  45802  blengt1fldiv2p1  45917  2arymaptf1  45977  resum2sqorgt0  46033  reorelicc  46034  rrx2plordisom  46047  rrx2linest  46066  rrxsphere  46072  line2ylem  46075  itsclc0xyqsol  46092  itscnhlinecirc02p  46109  mo0sn  46139  thincn0eu  46291