Theorem expcom 116

Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
exp.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
expcom	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 30	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  561  pm4.79dc  911  dedlema  978  dedlemb  979  19.35-1  1673  cbval2  1970  cbvex2  1971  nelelne  2495  r19.21be  2624  r19.35-1  2684  mosubt  2984  sbcrext  3110  uneqdifeqim  3582  ssuni  3920  uniss2  3929  elpwuni  4065  elssabg  4243  elpw2g  4251  epelg  4393  elomssom  4709  relop  4886  riinint  4999  cnviinm  5285  funopg  5367  fun  5516  tz6.12c  5678  fvelrnb  5702  fmptco  5821  funopsn  5838  fnressn  5848  fressnfv  5849  fvtp2g  5871  fvtp3g  5872  fconst2g  5877  isores3  5966  isoselem  5971  eloprabga  6118  fo1stresm  6333  poxp  6406  fsuppeq  6425  suppssdc  6438  brtpos2  6460  smores  6501  tfrlem1  6517  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  frecrdg  6617  oawordriexmid  6681  nnacl  6691  nnmcl  6692  nnacom  6695  nnaass  6696  nnmsucr  6699  nndifsnid  6718  nnmordi  6727  iinerm  6819  th3qlem2  6850  elpmg  6876  pmss12g  6887  mapsn  6902  brdomg  6962  f1domg  6974  ssdomg  6995  nndomo  7093  elfi2  7214  nnnninfeq2  7371  carden2bex  7437  cc3  7530  addclpi  7590  addnidpig  7599  genpassl  7787  genpassu  7788  nqprloc  7808  ltaprlem  7881  recexprlemopl  7888  recexprlemopu  7890  recexprlemupu  7891  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemupu  7912  caucvgprlemupu  7935  caucvgprprlemupu  7963  archsr  8045  peano2nnnn  8116  receuap  8892  peano2nn  9198  nnaddcl  9206  zrevaddcl  9573  nzadd  9575  zdiv  9611  nneo  9626  zeo2  9629  peano5uzti  9631  fzind  9638  fnn0ind  9639  lbzbi  9893  qrevaddcl  9921  irradd  9923  irrmul  9924  ltsubrp  9968  ltaddrp  9969  xnn0xadd0  10145  icoshft  10268  fzen  10321  elfzm11  10369  uzsplit  10370  fzoval  10426  elfzom1elp1fzo  10491  exfzdc  10530  modaddmodup  10693  frec2uzrdg  10715  nninfinf  10749  seq3clss  10777  monoord  10791  seq3caopr3  10797  seqcaopr3g  10798  seq3f1olemp  10821  seqf1oglem2a  10824  seqf1og  10827  seq3id3  10830  seq3homo  10833  seq3z  10834  seqfeq4g  10837  ser3ge0  10842  expadd  10887  expmul  10890  leexp1a  10900  modqexp  10972  faccl  11041  facdiv  11044  faclbnd  11047  faclbnd6  11050  omgadd  11109  hashunsng  11115  seq3coll  11150  fundm2domnop0  11156  swrdswrdlem  11332  swrdswrd  11333  wrd2ind  11351  swrdccatin1  11353  swrdccatin2  11357  pfxccatin12lem2  11359  pfxccat3  11362  shftlem  11437  resqrexlemover  11631  resqrexlemdecn  11633  resqrexlemlo  11634  resqrexlemcalc3  11637  climub  11965  climserle  11966  fsumzcl2  12027  fsumsplitsnun  12041  fsum2d  12057  modfsummodlemstep  12079  fsumabs  12087  fsumiun  12099  bcxmas  12111  cvgratnnlemnexp  12146  cvgratnnlemmn  12147  prodfap0  12167  prodfrecap  12168  ntrivcvgap  12170  prodmodc  12200  fprodssdc  12212  fprodabs  12238  fprod2d  12245  dvdsmod0  12415  dvds2ln  12446  dvdsabseq  12469  dvdsdivcl  12472  alzdvds  12476  oddnn02np1  12502  m1exp1  12523  nn0o1gt2  12527  nno  12528  ndvdsadd  12553  flodddiv4  12558  bitsinv1  12584  gcddiv  12651  gcdmultiple  12652  gcdmultiplez  12653  rplpwr  12659  dvdssq  12663  nninfct  12673  nn0seqcvgd  12674  alginv  12680  algcvga  12684  algfx  12685  isprm2  12750  isprm3  12751  prmdvdsexp  12781  eulerthlemrprm  12862  eulerthlema  12863  pcmpt  12977  ennnfoneleminc  13093  ennnfonelemkh  13094  ennnfonelemhf1o  13095  ennnfonelemhom  13097  omiunct  13126  nninfdclemlt  13133  setsn0fun  13180  mgmcl  13503  dfgrp3mlem  13742  mhmmulg  13811  resghm2b  13910  gsumfzconst  13989  srgpcomp  14065  lmodfopnelem1  14400  rmodislmodlem  14426  lss1d  14459  cnfldmulg  14652  cnfldexp  14653  gsumfzfsumlemm  14663  restopnb  14972  restdis  14975  tgcnp  15000  cnntr  15016  cnsscnp  15020  txcn  15066  txlm  15070  mettri  15164  blssexps  15220  blssex  15221  mopni3  15275  metss  15285  dvmptfsum  15516  plycolemc  15549  rpcxpmul2  15704  gausslemma2dlem6  15866  lgsquad2lem2  15881  2lgslem1c  15889  2lgslem3  15900  2lgs  15903  uhgredgrnv  16059  usgruspgrben  16107  usgredg2vlem2  16144  subupgr  16194  uspgr2wlkeq  16286  clwwlkccatlem  16321  umgrclwwlkge2  16323  clwwlkn1loopb  16341  clwwlknonex2lem2  16359  eupth2lem3lem4fi  16394  eupth2fi  16400  2spim  16464  exmidcon  16708