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 ⊢ (𝜓 → (𝜑 → 𝜒))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  565  pm4.79dc  915  dedlema  982  dedlemb  983  19.35-1  1677  cbval2  1977  cbvex2  1978  nelelne  2512  r19.21be  2641  r19.35-1  2701  mosubt  3003  sbcrext  3129  uneqdifeqim  3613  ssuni  3957  uniss2  3966  elpwuni  4102  elssabg  4284  elpw2g  4292  epelg  4435  elomssom  4752  relop  4930  riinint  5043  cnviinm  5329  funopg  5411  fun  5561  tz6.12c  5725  fvelrnb  5750  fmptco  5874  funopsn  5891  fnressn  5901  fressnfv  5902  fvtp2g  5924  fvtp3g  5925  fconst2g  5930  isores3  6021  isoselem  6026  eloprabga  6175  fo1stresm  6395  poxp  6468  fsuppeq  6487  suppssdc  6500  brtpos2  6522  smores  6563  tfrlem1  6579  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecrdg  6679  oawordriexmid  6743  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nnmsucr  6761  nndifsnid  6780  nnmordi  6789  iinerm  6881  th3qlem2  6912  elpmg  6938  pmss12g  6956  mapsn  6972  brdomg  7032  f1domg  7044  ssdomg  7065  nndomo  7165  ffsuppbi  7300  elfi2  7306  nnnninfeq2  7469  carden2bex  7535  cc3  7634  addclpi  7694  addnidpig  7703  genpassl  7891  genpassu  7892  nqprloc  7912  ltaprlem  7985  recexprlemopl  7992  recexprlemopu  7994  recexprlemupu  7995  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemupu  8016  caucvgprlemupu  8039  caucvgprprlemupu  8067  archsr  8149  peano2nnnn  8220  receuap  9000  indval0  9298  peano2nn  9317  nnaddcl  9325  zrevaddcl  9697  nzadd  9699  zdiv  9736  nneo  9751  zeo2  9754  peano5uzti  9756  fzind  9763  fnn0ind  9764  lbzbi  10018  qrevaddcl  10046  irradd  10048  irrmul  10049  ltsubrp  10093  ltaddrp  10094  xnn0xadd0  10271  icoshft  10394  fzen  10449  elfzm11  10500  uzsplit  10501  fzoval  10557  elfzom1elp1fzo  10622  exfzdc  10661  modaddmodup  10826  frec2uzrdg  10848  nninfinf  10882  seq3clss  10910  monoord  10924  seq3caopr3  10930  seqcaopr3g  10931  seq3f1olemp  10954  seqf1oglem2a  10957  seqf1og  10960  seq3id3  10963  seq3homo  10966  seq3z  10967  seqfeq4g  10970  ser3ge0  10975  expadd  11020  expmul  11023  leexp1a  11033  modqexp  11106  faccl  11175  facdiv  11178  faclbnd  11181  faclbnd6  11184  omgadd  11244  hashunsng  11250  hashmap  11270  hashf1  11289  seq3coll  11296  fundm2domnop0  11302  swrdswrdlem  11478  swrdswrd  11479  wrd2ind  11497  swrdccatin1  11499  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccat3  11508  shftlem  11583  resqrexlemover  11778  resqrexlemdecn  11780  resqrexlemlo  11781  resqrexlemcalc3  11784  climub  12112  climserle  12113  fsumzcl2  12174  fsumsplitsnun  12188  fsum2d  12204  modfsummodlemstep  12226  fsumabs  12234  fsumiun  12246  bcxmas  12258  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  prodfap0  12314  prodfrecap  12315  ntrivcvgap  12317  prodmodc  12347  fprodssdc  12359  fprodabs  12385  fprod2d  12392  dvdsmod0  12562  dvds2ln  12593  dvdsabseq  12616  dvdsdivcl  12619  alzdvds  12623  oddnn02np1  12649  m1exp1  12670  nn0o1gt2  12674  nno  12675  ndvdsadd  12700  flodddiv4  12705  bitsinv1  12731  gcddiv  12798  gcdmultiple  12799  gcdmultiplez  12800  rplpwr  12806  dvdssq  12810  nninfct  12820  nn0seqcvgd  12821  alginv  12827  algcvga  12831  algfx  12832  isprm2  12897  isprm3  12898  prmdvdsexp  12928  eulerthlemrprm  13009  eulerthlema  13010  pcmpt  13124  ennnfoneleminc  13304  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemhom  13308  omiunct  13337  nninfdclemlt  13344  setsn0fun  13391  mgmcl  13681  dfgrp3mlem  13905  mhmmulg  13968  resghm2b  14067  gzsumconst  14145  srgpcomp  14296  lmodfopnelem1  14663  rmodislmodlem  14689  lss1d  14722  cnfldmulg  14915  cnfldexp  14916  restopnb  15284  restdis  15287  tgcnp  15312  cnntr  15328  cnsscnp  15332  txcn  15378  txlm  15382  mettri  15476  blssexps  15532  blssex  15533  mopni3  15587  metss  15597  dvmptfsum  15828  plycolemc  15861  rpcxpmul2  16021  bcmono  16124  gausslemma2dlem6  16198  lgsquad2lem2  16213  2lgslem1c  16221  2lgslem3  16232  2lgs  16235  uhgredgrnv  16391  usgruspgrben  16439  usgredg2vlem2  16476  subupgr  16526  uspgr2wlkeq  16618  clwwlkccatlem  16653  umgrclwwlkge2  16655  clwwlkn1loopb  16673  clwwlknonex2lem2  16691  eupth2lem3lem4fi  16726  eupth2fi  16732  2spim  16806  exmidcon  17049  alsralrex  17165