Theorem expcom 419

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancoms  464  pm3.21  477  sylan  592  animpimp2impd  860  4casesdan  1057  dedlema  1061  dedlemb  1062  sbiedvw  2132  mo4  2592  2moswapv  2655  2moswap  2670  2eu2  2678  pm2.61ne  3041  nelelne  3057  r19.21be  3256  rspcebdv  3571  2reu2  3846  csbie2df  4401  minel  4419  uneqdifeq  4448  raltpd  4742  ssunsn2  4788  opthprneg  4825  ssuni  4893  uniss2  4902  elpwuni  5065  intss2  5068  disjord  5092  elpw2g  5295  elssabg  5304  axprglem  5394  oteqex  5472  otsndisj  5492  otiunsndisj  5493  epelg  5552  wereu  5647  relop  5828  riinint  5954  sotri3  6124  unixpid  6286  reuop  6295  ordtr2  6407  ordsssuc2  6455  iotan0  6527  funopg  6572  fun  6742  fvmptnf  7014  fvn0ssdmfun  7072  eldmrexrnb  7090  fmptco  7128  fnressn  7160  fressnfv  7162  fprb  7197  fvtp2g  7202  fvtp3g  7203  fconst2g  7207  fntpb  7213  f1dom3el3dif  7271  f1ounsn  7278  isores3  7341  isoselem  7347  oprabv  7478  eloprabga  7527  sorpsscmpl  7748  difex2  7772  ordpwsuc  7824  ordsucun  7834  limuni3  7861  trom  7884  fo1stres  8025  poxp  8138  soxp  8139  xpord3inddlem  8164  soseq  8169  suppimacnv  8184  fsuppeq  8185  funsssuppss  8200  brtpos2  8242  frrlem8  8304  fpr2a  8313  onnseq  8345  smores  8353  smofvon2  8357  tfrlem1  8376  oacl  8536  omcl  8537  oecl  8538  oawordri  8551  oalimcl  8561  oaass  8562  oarec  8563  omwordri  8573  omeulem1  8583  omeulem2  8584  oeordi  8589  oeworde  8595  oeoelem  8600  nnacl  8613  nnmcl  8614  nnecl  8615  nnacom  8619  nnaass  8624  nnmsucr  8627  nnmordi  8633  omabs  8653  cofonr  8676  naddunif  8696  iiner  8803  elpmg  8856  fsetfcdm  8875  fsetprcnex  8877  pmss12g  8890  mapfvd  8900  f1domg  8991  ssdomg  9020  undom  9077  domtriord  9135  ssnnfi  9178  fnfi  9186  enfi  9195  php  9215  sdom1  9234  1sdom2dom  9238  fisseneq  9247  isinf  9249  dif1ennnALT  9261  findcard3  9267  frfi  9269  difinf  9296  iunfi  9325  fsuppunfi  9373  fsuppres  9378  ffsuppbi  9383  elfi2  9399  marypha1lem  9418  marypha1  9419  oiexg  9522  wemapso2  9540  harword  9550  brwdom  9554  unxpwdom  9576  en3lplem1  9606  inf3lemd  9621  inf3lem5  9626  cantnfval2  9663  cantnfle  9665  cantnflt  9666  cnfcom  9694  tcmin  9733  frr2  9757  r1sdom  9774  rankxplim3  9891  elhf2  9903  elhf3OLD  9916  hfpw  9919  cardidm  10033  cardmin2  10073  infxpenlem  10085  fseqenlem1  10096  numacn  10121  alephordi  10146  iscard3  10165  alephinit  10167  carduniima  10168  iunfictbso  10186  dfac5  10200  dfac12lem3  10217  nnadju  10269  pwsdompw  10274  pwdjudom  10286  cflim2  10334  cfslb2n  10339  cofsmo  10340  cfsmolem  10341  cfcoflem  10343  alephsing  10347  infpssALT  10384  fin23lem34  10417  isf32lem2  10425  isf32lem10  10433  isf32lem12  10435  isfin1-2  10456  hsmexlem4  10500  axcc2lem  10507  domtriomlem  10513  axdc2lem  10519  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  axcclem  10528  ac6num  10550  ac6s  10555  zorn2lem7  10573  ttukeylem5  10584  imadomg  10606  iundom2g  10617  ondomon  10640  ficard  10642  konigthlem  10646  alephreg  10660  pwcfsdom  10661  cfpwsdom  10662  axregndlem1  10680  axregnd  10682  pwfseqlem3  10738  pwxpndom2  10743  pwxpndom  10744  pwdjundom  10745  inawinalem  10767  gchina  10777  wuncval2  10825  tsk0  10841  tskxpss  10850  inatsk  10856  tskuni  10861  gruina  10896  grothac  10908  addclpi  10970  addnidpi  10979  nqereu  11007  mulcanenq  11038  genpnnp  11083  nqpr  11092  prlem934  11111  reclem2pr  11126  suplem1pr  11130  supsrlem  11189  axpre-sup  11247  1re  11301  dedekindle  11467  00id  11478  receu  11954  sup3  12267  infrelb  12295  peano5nni  12331  nnindd  12348  nnaddcl  12351  zrevaddcl  12734  nzadd  12737  zdiv  12762  nneo  12776  zeo2  12779  nn0indd  12789  fzind  12790  fnn0ind  12791  fzindd  12794  uzwo  13031  lbzbi  13056  nn01to3  13061  qrevaddcl  13092  irradd  13094  irrmul  13095  ltsubrp  13151  ltaddrp  13152  xnn0xaddcl  13358  xnn0xadd0  13370  icoshft  13597  fzen  13667  elfzm11  13722  uzsplit  13723  elfzom1elp1fzo  13860  fzoopth  13890  injresinjlem  13918  injresinj  13919  modifeq2int  14069  modsumfzodifsn  14080  om2uzlti  14086  ssnn0fi  14121  fsuppmapnn0fiub0  14129  mptnn0fsuppr  14135  seqcaopr3  14173  seqf1olem2a  14176  seqf1o  14179  ser1const  14194  expadd  14240  expmul  14243  leexp1a  14311  faccl  14420  facdiv  14424  faclbnd  14427  faclbnd4lem4  14433  hasheqf1oi  14488  hashgadd  14514  hashinfxadd  14522  hashunx  14523  hashunsng  14529  elprchashprn2  14533  hashss  14546  hash1snb  14557  hashmap  14573  hashf1lem2  14594  hashf1  14595  seqcoll  14602  hashle2pr  14615  hashdmpropge2  14621  hashge3el3dif  14625  hash1to3  14630  fundmge2nop0  14640  fi1uzind  14645  brfi1indALT  14648  sswrd  14660  swrdnd2  14798  swrdnnn0nd  14799  swrdnd0  14800  swrdwrdsymb  14805  pfxnd0  14831  swrdswrdlem  14846  swrdswrd  14847  wrd2ind  14865  swrdccatin1  14867  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccat3  14876  repsdf2  14922  repswswrd  14928  cshw0  14938  cshwcl  14942  cshwlen  14943  cshf1  14954  swrdco  14981  relexpsucnnl  15176  rtrclreclem3  15206  rtrclreclem4  15207  relexpindlem  15209  rtrclind  15211  shftlem  15214  sgn3da  15247  caubnd  15519  reusq0  15625  rlimcld2  15738  o1dif  15790  climub  15822  climserle  15823  iseraltlem2  15843  sumss  15883  fsumzcl2  15898  fsummsnunz  15913  fsumsplitsnun  15914  fsum2d  15930  modfsummods  15953  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  climcndslem1  16011  climcndslem2  16012  cvgrat  16045  clim2prod  16050  prodfn0  16056  prodfrec  16057  ntrivcvg  16059  prodmo  16096  fprodss  16108  fprodabs  16134  fprodn0  16139  fprod2d  16141  fprodefsum  16254  ruclem8  16398  ruclem9  16399  dvdsmod0  16421  dvds2ln  16452  dvdsaddre2b  16470  dvdslelem  16472  dvdsdivcl  16479  alzdvds  16483  mod2eq1n2dvds  16510  oddnn02np1  16511  nn0o1gt2  16544  nno  16545  sumeven  16550  sumodd  16551  pwp1fsum  16554  ndvdsadd  16573  bitsinv1  16605  sadcadd  16621  sadadd2  16623  saddisjlem  16627  smuval2  16645  smupvallem  16646  smu01lem  16648  smupval  16651  smueqlem  16653  smumullem  16655  gcddiv  16717  rplpwr  16725  nn0seqcvgd  16738  seq1st  16739  alginv  16743  algcvga  16747  algfx  16748  absprodnn  16786  isprm2  16850  isprm3  16851  prmind2  16853  maxprmfct  16878  prmdvdsexp  16884  pcmpt  17063  prmreclem4  17090  vdwmc2  17150  vdwlem10  17161  ramub2  17185  ramcl  17200  prmgaplem5  17226  prmgaplem8  17229  cshwshashlem1  17266  cshwshashlem3  17268  setsn0fun  17344  imasleval  17706  divsfval  17712  mreexexlem4d  17814  isssc  17988  initoeu1  18179  termoeu1  18186  istos  18583  chnfibg  18803  mgmcl  18812  sgrpidmnd  18921  frmdgsum  19051  smndex1mgm  19099  dfgrp3lem  19241  mhmmulg  19318  resghm2b  19441  gsumwrev  19573  elsymgbas  19581  symgextf1  19628  gsmsymgreqlem2  19638  gsmsymgreq  19639  odlem1  19742  odcl2  19772  gexlem1  19786  efgi2  19932  efginvrel2  19934  efgsrel  19941  cyggexb  20106  gsummulglem  20148  gsumzunsnd  20163  gsum2dlem2  20178  telgsums  20200  dmdprd  20207  dprdw  20219  ablfac1eulem  20281  srgpcomp  20437  rnghmmul  20672  nrhmzr  20782  lmodfopnelem1  21166  rmodislmodlem  21197  cnfldmulg  21703  cnfldexp  21704  nzerooringczr  21779  obslbs  22029  mplcoe1  22339  mplcoe3  22340  mplcoe5  22342  cply1mul  22607  coe1fzgsumdlem  22614  gsummoncoe1  22619  pf1ind  22666  evl1gsumdlem  22667  mat1dimcrng  22785  ma1repveval  22879  mulmarep1gsum2  22882  gsummatr01lem3  22965  matunitlindflem1  22987  cramerlem3  23000  decpmatmulsumfsupp  23084  mp2pm2mplem4  23120  pm2mpmhmlem1  23129  fvmptnn04if  23160  cayhamlem1  23177  fctop  23315  mretopd  23403  restopnb  23486  restdis  23489  tgcnp  23564  cncls2  23584  cncls  23585  cnntr  23586  cnsscnp  23590  cmpsub  23711  2ndcsep  23771  1stcelcls  23773  lfinpfin  23836  locfincmp  23838  comppfsc  23844  txcn  23938  txlm  23960  xkohaus  23965  qtopres  24010  haushmphlem  24099  cmphmph  24100  connhmph  24101  reghmph  24105  nrmhmph  24106  ptcmpfi  24125  reghaus  24137  fbssfi  24149  fbun  24152  fbfinnfr  24153  isfildlem  24169  fgcl  24190  cfinfil  24205  supfil  24207  ufinffr  24241  fin1aufil  24244  cnpflf  24313  alexsubALTlem3  24361  alexsubALT  24363  cnextfvval  24377  cnextcn  24379  tmdgsum  24407  tgphaus  24429  tgpt1  24430  mettri  24664  blssexps  24738  blssex  24739  mopni3  24806  metss  24820  psmetutop  24879  dscmet  24884  tngngp3  24968  rectbntr0  25145  metnrmlem1a  25171  fsumcn  25184  lmmbr  25572  caubl  25622  caublcls  25623  bcthlem5  25642  bcth3  25645  ovolunlem1a  25810  ovoliunnul  25821  finiunmbl  25858  voliunlem1  25864  volsuplem  25869  volsup  25870  dyadmax  25912  itgfsum  26140  dvnadd  26242  cpnord  26248  dvnfre  26265  dvmptfsum  26288  dvlip  26306  fta1g  26481  plyco  26553  dgrcolem1  26585  dgrco  26587  dvnply2  26601  plydivex  26611  plyexmo  26629  aannenlem1  26648  aaliou3lem2  26663  dvntaylp  26691  taylthlem1  26693  ulmval  26700  cxpmul2  27010  cxpsqrtth  27051  scvxcvx  27306  jensenlem2  27308  jensen  27309  ppiub  27524  bcmono  27597  bpos1lem  27602  bposlem5  27608  gausslemma2dlem6  27692  lgsquad2lem2  27705  2lgslem3  27724  2lgs  27727  2sqnn  27759  addsqnreup  27763  2sqreultblem  27768  2sqreunnltblem  27771  dchrisumlem1  27809  dchrisum0flb  27830  pntpbnd1  27906  pntlemf  27925  qabvle  27945  qabvexp  27946  ostthlem2  27948  ostth2lem2  27954  ltsval2  28006  ltssolem1  28025  negsprop  28414  mulsuniflem  28528  precsexlem6  28591  precsexlem7  28592  noseqind  28671  om2noseqlt  28678  n0addscl  28723  n0mulscl  28724  expsne0  28815  axeuclidlem  29533  axcontlem12  29546  umgrnloopv  29677  uhgredgrnv  29701  edglnl  29714  numedglnl  29715  usgruspgrb  29757  usgrnloopvALT  29775  usgredg2vlem2  29800  subupgr  29861  nbumgr  29921  uhgrnbgr0nb  29928  nbgr0edglem  29930  edgusgrnbfin  29947  nb3grprlem2  29955  uvtxnbgrvtx  29967  cplgrop  30011  cusgrfi  30032  fusgrmaxsize  30038  fusgrn0degnn0  30073  ewlkprop  30177  uspgr2wlkeq  30219  g0wlk0  30224  wlkreslem  30241  subgrwlk  30262  lfgriswlk  30264  upgrwlkdvde  30316  spthonepeq  30331  uhgrwkspth  30334  usgr2trlncl  30339  usgr2trlspth  30340  cyclnumvtx  30381  cyclnspth  30382  crctcshwlkn0lem3  30394  wwlksn  30419  wspthneq1eq2  30442  wwlksm1edg  30463  wwlksnred  30474  wwlksnextfun  30480  wwlksnextinj  30481  wwlksnextproplem3  30493  wspthsnonn0vne  30499  wspn0  30506  rusgrnumwwlk  30560  clwwlkccatlem  30573  umgrclwwlkge2  30575  clwlkclwwlklem2  30584  clwlkclwwlklem3  30585  clwwisshclwws  30599  clwwisshclwwsn  30600  clwwlkn1loopb  30627  wwlksext2clwwlk  30641  wwlksubclwwlk  30642  clwwlknonex2lem2  30692  upgr3v3e3cycl  30774  uhgr3cyclex  30776  upgr4cycl4dv4e  30779  eupth2lem3lem4  30825  eupth2lem3lem7  30828  eupth2  30833  eulerpath  30835  nfrgr2v  30866  frgr3vlem1  30867  3vfriswmgr  30872  1to2vfriswmgr  30873  1to3vfriswmgr  30874  3cyclfrgrrn1  30879  3cyclfrgrrn  30880  3cyclfrgrrn2  30881  4cycl2vnunb  30884  frgrncvvdeqlem2  30894  frgrncvvdeqlem8  30900  frgrncvvdeqlem9  30901  frgrwopreglem4a  30904  frgrwopreglem5lem  30914  frgrwopreglem5ALT  30916  frgrregorufr0  30918  frgr2wwlk1  30923  frgr2wwlkeqm  30925  fusgr2wsp2nb  30928  2wspmdisj  30931  frrusgrord  30935  numclwwlk1lem2f1  30951  numclwlk1  30965  frgrreggt1  30987  friendshipgt3  30992  hlim2  31787  elnlfn  32523  stle0i  32834  hstrbi  32861  spansncv2  32888  h1da  32944  fmptcof2  33244  xreceu  33481  domnprodn0  33832  1arithufdlem3  34071  1arithufdlem4  34072  tpr2rico  34537  hasheuni  34710  ismeas  34825  sseqp1  35020  rrvsum  35079  dstfrvunirn  35100  signstfvc  35196  bnj607  35539  bnj1145  35616  bnj1204  35635  fineqvrep  35765  fineqvnttrclselem1  35772  onvf1odlem4  35868  vonf1oonfo  35877  fisshasheq  35882  subfacp1lem6  35929  cvmlift2lem12  36058  cvmlift3lem4  36066  satfrnmapom  36114  sat1el2xp  36123  satffunlem2  36152  satffun  36153  mrsubvrs  36266  climuzcnv  36415  iprodefisumlem  36484  dfon2lem9  36533  linethru  36898  finminlem  37086  fnessref  37125  neibastop2lem  37128  fnemeet2  37135  nndivsub  37225  bj-cbvew  37521  bj-xpnzex  37852  bj-elpwg  37947  bj-epelg  37963  bj-axseprep  37970  mptsnunlem  38241  dissneqlem  38243  topdifinffinlem  38250  iooelexlt  38265  domalom  38307  fvineqsneq  38315  wl-exeq  38446  poimirlem22  38540  poimirlem26  38544  poimirlem28  38546  poimirlem29  38547  poimirlem32  38550  heicant  38553  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  cover2  38629  upixp  38643  sdclem2  38656  fdc  38659  seqpo  38661  metf1o  38669  mettrifi  38671  sstotbnd3  38690  heibor1lem  38723  heiborlem5  38729  heibor  38735  bfplem1  38736  elghomlem2OLD  38800  grpokerinj  38807  isrngo  38811  rngodm1dm2  38846  ispridl2  38952  exlimddvf  39033  lssatle  40052  4atexlemex4  41110  uzindd  43008  evl1gprodd  43147  sn-axprlem3  43252  redvmptabs  43391  sn-sup3d  43536  mzpsubst  43738  jm2.18  43974  wepwsolem  44028  oaabsb  44280  oacl2g  44316  ofoafg  44340  ofoaid1  44344  ofoaid2  44345  naddonnn  44381  iunrelexp0  44687  relexpmulg  44695  cnvtrclfv  44709  clsk1indlem3  45028  grucollcld  45229  inaex  45266  dvgrat  45281  radcnvrat  45283  csbxpgVD  45861  sineq0ALT  45904  trfr  45930  relwf  45935  pwclaxpow  45952  omssaxinf2  45956  islptre  46600  iblspltprt  46952  stoweidlem2  46981  stoweidlem17  46996  stoweidlem21  47000  2reuimp0  48153  2reuimp  48154  afveu  48192  funbrafv  48197  ndmaovass  48245  afv2eu  48277  tz6.12c-afv2  48281  funop1  48322  f1oresf1o2  48330  fvmptrabdm  48332  nltle2tri  48352  2elfz2melfz  48357  fsummsndifre  48419  fsumsplitsndif  48420  fsummmodsndifre  48421  fsummmodsnunz  48422  elsetpreimafvssdm  48437  uniimaelsetpreimafv  48447  imasetpreimafvbijlemfv1  48454  iccpartiltu  48473  iccpartigtl  48474  iccpartleu  48479  iccpartgel  48480  iccpartrn  48481  iccpartiun  48485  icceuelpart  48487  iccpartnel  48489  fargshiftf  48491  fargshiftf1  48492  ichnfb  48516  elsprel  48526  prsprel  48538  sprsymrelfo  48548  paireqne  48562  sbcpr  48572  reupr  48573  fmtnoinf  48590  odz2prm2pw  48617  lighneallem4  48664  lighneal  48665  requad1  48689  requad2  48690  evensumeven  48774  even3prm2  48786  gbowgt5  48829  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbnnsum3prm  48871  bgoldbtbndlem2  48873  bgoldbtbndlem4  48875  bgoldbtbnd  48876  dfsclnbgr6  48925  grimco  48956  cycl3grtri  49014  isubgr3stgrlem6  49038  gricgrlic  49085  gpgedgvtx0  49128  gpgprismgr4cycllem3  49164  pgnbgreunbgrlem5  49190  clcllaw  49257  rngccatidALTV  49338  ringccatidALTV  49372  scmsuppss  49452  gsumlsscl  49461  ply1mulgsumlem2  49468  lincvalsc0  49502  linc0scn0  49504  lincdifsn  49505  linc1  49506  lincellss  49507  lincsum  49510  lincscm  49511  lincsumcl  49512  lcoss  49517  lincext3  49537  lindslinindimp2lem4  49542  lindslinindsimp2lem5  49543  lindslinindsimp2  49544  lindsrng01  49549  snlindsntor  49552  lincresunit3lem2  49561  lincresunit3  49562  islindeps2  49564  blengt1fldiv2p1  49674  2arymaptf1  49734  resum2sqorgt0  49790  reorelicc  49791  rrx2plordisom  49804  rrx2linest  49823  rrxsphere  49829  line2ylem  49832  itsclc0xyqsol  49849  itscnhlinecirc02p  49866  mo0sn  49895  thincn0eu  50508  alsralrex  50877  alsraln0  50878