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  2097  cbval2vOLD  2342  mo4  2567  2moswapv  2632  2moswap  2647  2mos  2652  2eu2  2655  pm2.61ne  3031  nelelne  3044  r19.21be  3136  cbvraldva2  3393  rspcebdv  3556  2reu2  3832  csbie2df  4375  minel  4400  uneqdifeq  4424  raltpd  4718  ssunsn2  4761  opthprneg  4796  ssuni  4867  uniss2  4875  elpwuni  5035  intss2  5038  disjord  5063  elssabg  5261  elpw2g  5269  axprlem3  5349  axprlem4  5350  axprlem5  5351  oteqex  5415  otsndisj  5434  otiunsndisj  5435  epelg  5497  wereu  5586  relop  5762  riinint  5880  sotri3  6040  unixpid  6191  reuop  6200  ordtr2  6314  ordsssuc2  6358  iotan0  6427  funopg  6475  fun  6645  tz6.12c  6808  fvmptnf  6906  fvn0ssdmfun  6961  eldmrexrnb  6977  fmptco  7010  fnressn  7039  fressnfv  7041  fprb  7078  fvtp2g  7083  fvtp3g  7084  fconst2g  7087  fntpb  7094  f1dom3el3dif  7151  isores3  7215  isoselem  7221  oprabv  7344  eloprabga  7391  eloprabgaOLD  7392  sorpsscmpl  7596  difex2  7619  ordpwsuc  7671  ordsucun  7681  limuni3  7708  trom  7730  fo1stres  7866  poxp  7978  soxp  7979  suppimacnv  7999  frnsuppeq  8000  funsssuppss  8015  brtpos2  8057  frrlem8  8118  fpr2a  8127  wfrlem12OLD  8160  onnseq  8184  smores  8192  smofvon2  8196  tfrlem1  8216  oacl  8374  omcl  8375  oecl  8376  oawordri  8390  oalimcl  8400  oaass  8401  oarec  8402  omwordri  8412  omeulem1  8422  omeulem2  8423  oeordi  8427  oeworde  8433  oeoelem  8438  nnacl  8451  nnmcl  8452  nnecl  8453  nnacom  8457  nnaass  8462  nnmsucr  8465  nnmordi  8471  omabs  8490  iiner  8587  elpmg  8640  fsetfcdm  8657  fsetprcnex  8659  pmss12g  8666  mapfvd  8676  f1domg  8769  ssdomg  8795  undom  8855  domtriord  8919  ssnnfi  8961  ssnnfiOLD  8962  imafi  8967  fnfi  8973  enfi  8982  php  9002  phpOLD  9014  php3OLD  9016  1sdom  9034  fisseneq  9043  isinf  9045  dif1enALT  9059  findcard3  9066  frfi  9068  unfiOLD  9090  difinf  9093  iunfi  9116  fsuppunfi  9157  fsuppres  9162  frnfsuppbi  9166  elfi2  9182  marypha1lem  9201  marypha1  9202  oiexg  9303  wemapso2  9321  harword  9331  brwdom  9335  unxpwdom  9357  en3lplem1  9379  inf3lemd  9394  inf3lem5  9399  cantnfval2  9436  cantnfle  9438  cantnflt  9439  cnfcom  9467  tcmin  9508  frr2  9527  r1sdom  9541  rankxplim3  9648  cardidm  9726  cardmin2  9766  infxpenlem  9778  fseqenlem1  9789  numacn  9814  alephordi  9839  iscard3  9858  alephinit  9860  carduniima  9861  iunfictbso  9879  dfac5  9893  dfac12lem3  9910  nnadju  9962  pwsdompw  9969  pwdjudom  9981  cflim2  10028  cfslb2n  10033  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  alephsing  10041  infpssALT  10078  fin23lem34  10111  isf32lem2  10119  isf32lem10  10127  isf32lem12  10129  isfin1-2  10150  hsmexlem4  10194  axcc2lem  10201  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  ac6num  10244  ac6s  10249  zorn2lem7  10267  ttukeylem5  10278  imadomg  10299  iundom2g  10305  ondomon  10328  ficard  10330  konigthlem  10333  alephreg  10347  pwcfsdom  10348  cfpwsdom  10349  axregndlem1  10367  axregnd  10369  pwfseqlem3  10425  pwxpndom2  10430  pwxpndom  10431  pwdjundom  10432  inawinalem  10454  gchina  10464  wuncval2  10512  tsk0  10528  tskxpss  10537  inatsk  10543  tskuni  10548  gruina  10583  grothac  10595  addclpi  10657  addnidpi  10666  nqereu  10694  mulcanenq  10725  genpnnp  10770  nqpr  10779  prlem934  10798  reclem2pr  10813  suplem1pr  10817  supsrlem  10876  axpre-sup  10934  1re  10984  dedekindle  11148  00id  11159  receu  11629  sup3  11941  infrelb  11969  peano5nni  11985  nnindd  12002  nnaddcl  12005  zrevaddcl  12374  nzadd  12377  zdiv  12399  nneo  12413  zeo2  12416  nn0indd  12426  fzind  12427  fnn0ind  12428  fzindd  12431  uzwo  12660  lbzbi  12685  nn01to3  12690  qrevaddcl  12720  irradd  12722  irrmul  12723  ltsubrp  12775  ltaddrp  12776  xnn0xaddcl  12978  xnn0xadd0  12990  icoshft  13214  fzen  13282  elfzm11  13336  uzsplit  13337  elfzoext  13453  elfzom1elp1fzo  13463  injresinjlem  13516  injresinj  13517  modifeq2int  13662  modsumfzodifsn  13673  om2uzlti  13679  ssnn0fi  13714  fsuppmapnn0fiub0  13722  mptnn0fsuppr  13728  seqcaopr3  13767  seqf1olem2a  13770  seqf1o  13773  ser1const  13788  expadd  13834  expmul  13837  leexp1a  13902  faccl  14006  facdiv  14010  faclbnd  14013  faclbnd4lem4  14019  hasheqf1oi  14075  hashgadd  14101  hashinfxadd  14109  hashunx  14110  hashunsng  14116  elprchashprn2  14120  hashss  14133  hash1snb  14143  hashmap  14159  hashf1lem2  14179  hashf1  14180  seqcoll  14187  hashle2pr  14200  hashdmpropge2  14206  hashge3el3dif  14209  hash1to3  14214  fundmge2nop0  14215  fi1uzind  14220  brfi1indALT  14223  sswrd  14234  swrdnd2  14377  swrdnnn0nd  14378  swrdnd0  14379  swrdwrdsymb  14384  pfxnd0  14410  swrdswrdlem  14426  swrdswrd  14427  wrd2ind  14445  swrdccatin1  14447  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccat3  14456  repsdf2  14500  repswswrd  14506  cshw0  14516  cshwcl  14520  cshwlen  14521  cshf1  14532  swrdco  14559  relexpsucnnl  14750  rtrclreclem3  14780  rtrclreclem4  14781  relexpindlem  14783  rtrclind  14785  shftlem  14788  caubnd  15079  reusq0  15183  rlimcld2  15296  o1dif  15348  climub  15382  climserle  15383  iseraltlem2  15403  sumss  15445  fsumzcl2  15460  fsummsnunz  15475  fsumsplitsnun  15476  fsum2d  15492  modfsummods  15514  fsumabs  15522  fsumrlim  15532  fsumo1  15533  fsumiun  15542  climcndslem1  15570  climcndslem2  15571  cvgrat  15604  clim2prod  15609  prodfn0  15615  prodfrec  15616  ntrivcvg  15618  prodmo  15655  fprodss  15667  fprodabs  15693  fprodn0  15698  fprod2d  15700  fprodefsum  15813  ruclem8  15955  ruclem9  15956  dvdsmod0  15978  dvds2ln  16007  dvdsaddre2b  16025  dvdslelem  16027  dvdsdivcl  16034  alzdvds  16038  mod2eq1n2dvds  16065  oddnn02np1  16066  nn0o1gt2  16099  nno  16100  sumeven  16105  sumodd  16106  pwp1fsum  16109  ndvdsadd  16128  bitsinv1  16158  sadcadd  16174  sadadd2  16176  saddisjlem  16180  smuval2  16198  smupvallem  16199  smu01lem  16201  smupval  16204  smueqlem  16206  smumullem  16208  gcddiv  16268  gcdmultipleOLD  16269  rplpwr  16276  nn0seqcvgd  16284  seq1st  16285  alginv  16289  algcvga  16293  algfx  16294  absprodnn  16332  isprm2  16396  isprm3  16397  prmind2  16399  maxprmfct  16423  prmdvdsexp  16429  pcmpt  16602  prmreclem4  16629  vdwmc2  16689  vdwlem10  16700  ramub2  16724  ramcl  16739  prmgaplem5  16765  prmgaplem8  16768  cshwshashlem1  16806  cshwshashlem3  16808  setsn0fun  16883  imasleval  17261  divsfval  17267  mreexexlem4d  17365  isssc  17541  initoeu1  17735  termoeu1  17742  istos  18145  mgmcl  18338  sgrpidmnd  18399  frmdgsum  18510  smndex1mgm  18555  dfgrp3lem  18682  mhmmulg  18753  resghm2b  18861  gsumwrev  18982  elsymgbas  18990  symgextf1  19038  gsmsymgreqlem2  19048  gsmsymgreq  19049  odlem1  19152  odcl2  19181  gexlem1  19193  efgi2  19340  efginvrel2  19342  efgsrel  19349  cyggexb  19509  gsummulglem  19551  gsumzunsnd  19566  gsum2dlem2  19581  telgsums  19603  dmdprd  19610  dprdw  19622  ablfac1eulem  19684  srgpcomp  19777  lmodfopnelem1  20168  rmodislmodlem  20199  cnfldmulg  20639  cnfldexp  20640  obslbs  20946  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  cply1mul  21474  coe1fzgsumdlem  21481  gsummoncoe1  21484  pf1ind  21530  evl1gsumdlem  21531  mat1dimcrng  21635  ma1repveval  21729  mulmarep1gsum2  21732  gsummatr01lem3  21815  cramerlem3  21847  decpmatmulsumfsupp  21931  mp2pm2mplem4  21967  pm2mpmhmlem1  21976  fvmptnn04if  22007  cayhamlem1  22024  fctop  22163  mretopd  22252  restopnb  22335  restdis  22338  tgcnp  22413  cncls2  22433  cncls  22434  cnntr  22435  cnsscnp  22439  cmpsub  22560  2ndcsep  22619  1stcelcls  22621  lfinpfin  22684  locfincmp  22686  comppfsc  22692  txcn  22786  txlm  22808  xkohaus  22813  qtopres  22858  haushmphlem  22947  cmphmph  22948  connhmph  22949  reghmph  22953  nrmhmph  22954  ptcmpfi  22973  reghaus  22985  fbssfi  22997  fbun  23000  fbfinnfr  23001  isfildlem  23017  fgcl  23038  cfinfil  23053  supfil  23055  ufinffr  23089  fin1aufil  23092  cnpflf  23161  alexsubALTlem3  23209  alexsubALT  23211  cnextfvval  23225  cnextcn  23227  tmdgsum  23255  tgphaus  23277  tgpt1  23278  mettri  23514  blssexps  23588  blssex  23589  mopni3  23659  metss  23673  psmetutop  23732  dscmet  23737  tngngp3  23829  rectbntr0  24004  metnrmlem1a  24030  fsumcn  24042  lmmbr  24431  caubl  24481  caublcls  24482  bcthlem5  24501  bcth3  24504  ovolunlem1a  24669  ovoliunnul  24680  finiunmbl  24717  voliunlem1  24723  volsuplem  24728  volsup  24729  dyadmax  24771  itgfsum  25000  dvnadd  25102  cpnord  25108  dvnfre  25125  dvmptfsum  25148  dvlip  25166  fta1g  25341  plyco  25411  dgrcolem1  25443  dgrco  25445  dvnply2  25456  plydivex  25466  plyexmo  25482  aannenlem1  25497  aaliou3lem2  25512  dvntaylp  25539  taylthlem1  25541  ulmval  25548  cxpmul2  25853  cxpsqrtth  25893  scvxcvx  26144  jensenlem2  26146  jensen  26147  ppiub  26361  bcmono  26434  bpos1lem  26439  bposlem5  26445  gausslemma2dlem6  26529  lgsquad2lem2  26542  2lgslem3  26561  2lgs  26564  2sqnn  26596  addsqnreup  26600  2sqreultblem  26605  2sqreunnltblem  26608  dchrisumlem1  26646  dchrisum0flb  26667  pntpbnd1  26743  pntlemf  26762  qabvle  26782  qabvexp  26783  ostthlem2  26785  ostth2lem2  26791  axeuclidlem  27339  axcontlem12  27352  umgrnloopv  27485  uhgredgrnv  27509  edglnl  27522  numedglnl  27523  usgruspgrb  27560  usgrnloopvALT  27577  usgredg2vlem2  27602  subupgr  27663  nbumgr  27723  uhgrnbgr0nb  27730  nbgr0vtxlem  27731  edgusgrnbfin  27749  nb3grprlem2  27757  uvtxnbgrvtx  27769  cplgrop  27813  cusgrfi  27834  fusgrmaxsize  27840  fusgrn0degnn0  27875  ewlkprop  27979  uspgr2wlkeq  28022  g0wlk0  28028  wlkreslem  28046  lfgriswlk  28065  upgrwlkdvde  28114  spthonepeq  28129  uhgrwkspth  28132  usgr2trlncl  28137  usgr2trlspth  28138  cyclnspth  28177  crctcshwlkn0lem3  28186  wwlksn  28211  wspthneq1eq2  28234  wwlksm1edg  28255  wwlksnred  28266  wwlksnextfun  28272  wwlksnextinj  28273  wwlksnextproplem3  28285  wspthsnonn0vne  28291  wspn0  28298  rusgrnumwwlk  28349  clwwlkccatlem  28362  umgrclwwlkge2  28364  clwlkclwwlklem2  28373  clwlkclwwlklem3  28374  clwwisshclwws  28388  clwwisshclwwsn  28389  clwwlkn1loopb  28416  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwlknonex2lem2  28481  upgr3v3e3cycl  28553  uhgr3cyclex  28555  upgr4cycl4dv4e  28558  eupth2lem3lem4  28604  eupth2lem3lem7  28607  eupth2  28612  eulerpath  28614  nfrgr2v  28645  frgr3vlem1  28646  3vfriswmgr  28651  1to2vfriswmgr  28652  1to3vfriswmgr  28653  3cyclfrgrrn1  28658  3cyclfrgrrn  28659  3cyclfrgrrn2  28660  4cycl2vnunb  28663  frgrncvvdeqlem2  28673  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  frgrwopreglem4a  28683  frgrwopreglem5lem  28693  frgrwopreglem5ALT  28695  frgrregorufr0  28697  frgr2wwlk1  28702  frgr2wwlkeqm  28704  fusgr2wsp2nb  28707  2wspmdisj  28710  frrusgrord  28714  numclwwlk1lem2f1  28730  numclwlk1  28744  frgrreggt1  28766  friendshipgt3  28771  hlim2  29563  elnlfn  30299  stle0i  30610  hstrbi  30637  spansncv2  30664  h1da  30720  fmptcof2  31003  xreceu  31205  tpr2rico  31871  hasheuni  32062  ismeas  32176  sseqp1  32371  rrvsum  32430  dstfrvunirn  32450  sgn3da  32517  signstfvc  32562  bnj607  32905  bnj1145  32982  bnj1204  33001  fineqvrep  33073  fisshasheq  33082  subgrwlk  33103  subfacp1lem6  33156  cvmlift2lem12  33285  cvmlift3lem4  33293  satfrnmapom  33341  sat1el2xp  33350  satffunlem2  33379  satffun  33380  mrsubvrs  33493  climuzcnv  33638  iprodefisumlem  33715  dfon2lem9  33776  soseq  33812  sltval2  33868  sltsolem1  33887  linethru  34464  elhf2  34486  finminlem  34516  fnessref  34555  neibastop2lem  34558  fnemeet2  34565  nndivsub  34655  bj-xpnzex  35158  bj-elpwg  35234  bj-epelg  35248  mptsnunlem  35518  dissneqlem  35520  topdifinffinlem  35527  iooelexlt  35542  domalom  35584  fvineqsneq  35592  wl-exeq  35702  wl-ax11-lem3  35747  matunitlindflem1  35782  poimirlem22  35808  poimirlem26  35812  poimirlem28  35814  poimirlem29  35815  poimirlem32  35818  heicant  35821  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  cover2  35881  upixp  35896  sdclem2  35909  fdc  35912  seqpo  35914  metf1o  35922  mettrifi  35924  sstotbnd3  35943  heibor1lem  35976  heiborlem5  35982  heibor  35988  bfplem1  35989  elghomlem2OLD  36053  grpokerinj  36060  isrngo  36064  rngodm1dm2  36099  ispridl2  36205  exlimddvf  36288  lssatle  37036  4atexlemex4  38094  uzindd  39992  sn-axprlem3  40193  mzpsubst  40577  jm2.18  40817  wepwsolem  40874  iunrelexp0  41317  relexpmulg  41325  cnvtrclfv  41339  clsk1indlem3  41660  grucollcld  41885  inaex  41922  dvgrat  41937  radcnvrat  41939  csbxpgVD  42521  sineq0ALT  42564  islptre  43167  iblspltprt  43521  stoweidlem2  43550  stoweidlem17  43565  stoweidlem21  43569  2reuimp0  44617  2reuimp  44618  afveu  44656  funbrafv  44661  ndmaovass  44709  afv2eu  44741  tz6.12c-afv2  44745  funop1  44786  f1oresf1o2  44794  fvmptrabdm  44796  nltle2tri  44816  2elfz2melfz  44821  fzoopth  44830  fsummsndifre  44835  fsumsplitsndif  44836  fsummmodsndifre  44837  fsummmodsnunz  44838  elsetpreimafvssdm  44849  uniimaelsetpreimafv  44859  imasetpreimafvbijlemfv1  44866  iccpartiltu  44885  iccpartigtl  44886  iccpartleu  44891  iccpartgel  44892  iccpartrn  44893  iccpartiun  44897  icceuelpart  44899  iccpartnel  44901  fargshiftf  44903  fargshiftf1  44904  ichnfb  44928  elsprel  44938  prsprel  44950  sprsymrelfo  44960  paireqne  44974  sbcpr  44984  reupr  44985  fmtnoinf  44999  odz2prm2pw  45026  lighneallem4  45073  lighneal  45074  requad1  45085  requad2  45086  evensumeven  45170  even3prm2  45182  gbowgt5  45225  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  bgoldbtbndlem4  45271  bgoldbtbnd  45272  isomuspgrlem1  45290  clcllaw  45396  nrhmzr  45442  rnghmmul  45469  rngccatidALTV  45558  ringccatidALTV  45621  nzerooringczr  45641  scmsuppss  45719  gsumlsscl  45730  ply1mulgsumlem2  45739  lincvalsc0  45773  linc0scn0  45775  lincdifsn  45776  linc1  45777  lincellss  45778  lincsum  45781  lincscm  45782  lincsumcl  45783  lcoss  45788  lincext3  45808  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  lindslinindsimp2  45815  lindsrng01  45820  snlindsntor  45823  lincresunit3lem2  45832  lincresunit3  45833  islindeps2  45835  blengt1fldiv2p1  45950  2arymaptf1  46010  resum2sqorgt0  46066  reorelicc  46067  rrx2plordisom  46080  rrx2linest  46099  rrxsphere  46105  line2ylem  46108  itsclc0xyqsol  46125  itscnhlinecirc02p  46142  mo0sn  46172  thincn0eu  46324