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  1971  cbvex2  1972  nelelne  2504  r19.21be  2633  r19.35-1  2693  mosubt  2993  sbcrext  3119  uneqdifeqim  3594  ssuni  3935  uniss2  3944  elpwuni  4080  elssabg  4259  elpw2g  4267  epelg  4410  elomssom  4726  relop  4904  riinint  5017  cnviinm  5303  funopg  5385  fun  5535  tz6.12c  5699  fvelrnb  5723  fmptco  5842  funopsn  5859  fnressn  5869  fressnfv  5870  fvtp2g  5892  fvtp3g  5893  fconst2g  5898  isores3  5987  isoselem  5992  eloprabga  6139  fo1stresm  6354  poxp  6427  fsuppeq  6446  suppssdc  6459  brtpos2  6481  smores  6522  tfrlem1  6538  tfrlemi1  6562  tfr1onlemaccex  6578  tfrcllemaccex  6591  frecrdg  6638  oawordriexmid  6702  nnacl  6712  nnmcl  6713  nnacom  6716  nnaass  6717  nnmsucr  6720  nndifsnid  6739  nnmordi  6748  iinerm  6840  th3qlem2  6871  elpmg  6897  pmss12g  6908  mapsn  6924  brdomg  6984  f1domg  6996  ssdomg  7017  nndomo  7117  ffsuppbi  7252  elfi2  7258  nnnninfeq2  7419  carden2bex  7485  cc3  7581  addclpi  7641  addnidpig  7650  genpassl  7838  genpassu  7839  nqprloc  7859  ltaprlem  7932  recexprlemopl  7939  recexprlemopu  7941  recexprlemupu  7942  recexprlemss1l  7949  recexprlemss1u  7950  cauappcvgprlemupu  7963  caucvgprlemupu  7986  caucvgprprlemupu  8014  archsr  8096  peano2nnnn  8167  receuap  8942  peano2nn  9248  nnaddcl  9256  zrevaddcl  9627  nzadd  9629  zdiv  9665  nneo  9680  zeo2  9683  peano5uzti  9685  fzind  9692  fnn0ind  9693  lbzbi  9947  qrevaddcl  9975  irradd  9977  irrmul  9978  ltsubrp  10022  ltaddrp  10023  xnn0xadd0  10199  icoshft  10322  fzen  10376  elfzm11  10424  uzsplit  10425  fzoval  10481  elfzom1elp1fzo  10546  exfzdc  10585  modaddmodup  10748  frec2uzrdg  10770  nninfinf  10804  seq3clss  10832  monoord  10846  seq3caopr3  10852  seqcaopr3g  10853  seq3f1olemp  10876  seqf1oglem2a  10879  seqf1og  10882  seq3id3  10885  seq3homo  10888  seq3z  10889  seqfeq4g  10892  ser3ge0  10897  expadd  10942  expmul  10945  leexp1a  10955  modqexp  11027  faccl  11096  facdiv  11099  faclbnd  11102  faclbnd6  11105  omgadd  11164  hashunsng  11170  seq3coll  11210  fundm2domnop0  11216  swrdswrdlem  11392  swrdswrd  11393  wrd2ind  11411  swrdccatin1  11413  swrdccatin2  11417  pfxccatin12lem2  11419  pfxccat3  11422  shftlem  11497  resqrexlemover  11691  resqrexlemdecn  11693  resqrexlemlo  11694  resqrexlemcalc3  11697  climub  12025  climserle  12026  fsumzcl2  12087  fsumsplitsnun  12101  fsum2d  12117  modfsummodlemstep  12139  fsumabs  12147  fsumiun  12159  bcxmas  12171  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  prodfap0  12227  prodfrecap  12228  ntrivcvgap  12230  prodmodc  12260  fprodssdc  12272  fprodabs  12298  fprod2d  12305  dvdsmod0  12475  dvds2ln  12506  dvdsabseq  12529  dvdsdivcl  12532  alzdvds  12536  oddnn02np1  12562  m1exp1  12583  nn0o1gt2  12587  nno  12588  ndvdsadd  12613  flodddiv4  12618  bitsinv1  12644  gcddiv  12711  gcdmultiple  12712  gcdmultiplez  12713  rplpwr  12719  dvdssq  12723  nninfct  12733  nn0seqcvgd  12734  alginv  12740  algcvga  12744  algfx  12745  isprm2  12810  isprm3  12811  prmdvdsexp  12841  eulerthlemrprm  12922  eulerthlema  12923  pcmpt  13037  ennnfoneleminc  13154  ennnfonelemkh  13155  ennnfonelemhf1o  13156  ennnfonelemhom  13158  omiunct  13187  nninfdclemlt  13194  setsn0fun  13241  mgmcl  13564  dfgrp3mlem  13803  mhmmulg  13872  resghm2b  13971  gsumfzconst  14050  srgpcomp  14126  lmodfopnelem1  14464  rmodislmodlem  14490  lss1d  14523  cnfldmulg  14716  cnfldexp  14717  gsumfzfsumlemm  14727  restopnb  15038  restdis  15041  tgcnp  15066  cnntr  15082  cnsscnp  15086  txcn  15132  txlm  15136  mettri  15230  blssexps  15286  blssex  15287  mopni3  15341  metss  15351  dvmptfsum  15582  plycolemc  15615  rpcxpmul2  15770  gausslemma2dlem6  15932  lgsquad2lem2  15947  2lgslem1c  15955  2lgslem3  15966  2lgs  15969  uhgredgrnv  16125  usgruspgrben  16173  usgredg2vlem2  16210  subupgr  16260  uspgr2wlkeq  16352  clwwlkccatlem  16387  umgrclwwlkge2  16389  clwwlkn1loopb  16407  clwwlknonex2lem2  16425  eupth2lem3lem4fi  16460  eupth2fi  16466  2spim  16530  exmidcon  16772