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  7470  carden2bex  7536  cc3  7635  addclpi  7695  addnidpig  7704  genpassl  7892  genpassu  7893  nqprloc  7913  ltaprlem  7986  recexprlemopl  7993  recexprlemopu  7995  recexprlemupu  7996  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemupu  8017  caucvgprlemupu  8040  caucvgprprlemupu  8068  archsr  8150  peano2nnnn  8221  receuap  9002  indval0  9300  peano2nn  9319  nnaddcl  9327  zrevaddcl  9700  nzadd  9702  zdiv  9739  nneo  9754  zeo2  9757  peano5uzti  9759  fzind  9766  fnn0ind  9767  lbzbi  10026  qrevaddcl  10054  irradd  10056  irrmul  10058  ltsubrp  10102  ltaddrp  10103  xnn0xadd0  10280  icoshft  10403  fzen  10458  elfzm11  10509  uzsplit  10510  fzoval  10566  elfzom1elp1fzo  10631  exfzdc  10670  modaddmodup  10838  frec2uzrdg  10860  nninfinf  10894  seq3clss  10922  monoord  10936  seq3caopr3  10942  seqcaopr3g  10943  seq3f1olemp  10966  seqf1oglem2a  10969  seqf1og  10972  seq3id3  10975  seq3homo  10978  seq3z  10979  seqfeq4g  10982  ser3ge0  10987  expadd  11032  expmul  11035  leexp1a  11045  modqexp  11118  faccl  11188  facdiv  11191  faclbnd  11194  faclbnd6  11197  omgadd  11257  hashunsng  11263  hashmap  11283  hashf1  11302  seq3coll  11309  fundm2domnop0  11315  swrdswrdlem  11491  swrdswrd  11492  wrd2ind  11510  swrdccatin1  11512  swrdccatin2  11516  pfxccatin12lem2  11518  pfxccat3  11521  shftlem  11596  resqrexlemover  11791  resqrexlemdecn  11793  resqrexlemlo  11794  resqrexlemcalc3  11797  climub  12128  climserle  12129  fsumzcl2  12190  fsumsplitsnun  12204  fsum2d  12220  modfsummodlemstep  12242  fsumabs  12250  fsumiun  12262  bcxmas  12274  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  prodfap0  12330  prodfrecap  12331  ntrivcvgap  12333  prodmodc  12363  fprodssdc  12375  fprodabs  12401  fprod2d  12408  dvdsmod0  12578  dvds2ln  12609  dvdsabseq  12632  dvdsdivcl  12635  alzdvds  12639  oddnn02np1  12665  m1exp1  12686  nn0o1gt2  12690  nno  12691  ndvdsadd  12716  flodddiv4  12721  bitsinv1  12747  gcddiv  12814  gcdmultiple  12815  gcdmultiplez  12816  rplpwr  12822  dvdssq  12826  nninfct  12836  nn0seqcvgd  12837  alginv  12843  algcvga  12847  algfx  12848  isprm2  12913  isprm3  12914  prmdvdsexp  12945  eulerthlemrprm  13029  eulerthlema  13030  pcmpt  13144  ennnfoneleminc  13353  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ennnfonelemhom  13357  omiunct  13386  nninfdclemlt  13393  setsn0fun  13440  mgmcl  13730  dfgrp3mlem  13954  mhmmulg  14017  resghm2b  14116  gzsumconst  14194  srgpcomp  14345  lmodfopnelem1  14712  rmodislmodlem  14738  lss1d  14771  cnfldmulg  14964  cnfldexp  14965  restopnb  15334  restdis  15337  tgcnp  15362  cnntr  15378  cnsscnp  15382  txcn  15428  txlm  15432  mettri  15526  blssexps  15582  blssex  15583  mopni3  15637  metss  15647  dvmptfsum  15878  plycolemc  15911  rpcxpmul2  16071  ppiqub  16215  bcmono  16226  bpos1lem  16231  bposlem5  16237  gausslemma2dlem6  16308  lgsquad2lem2  16323  2lgslem1c  16331  2lgslem3  16342  2lgs  16345  uhgredgrnv  16501  usgruspgrben  16549  usgredg2vlem2  16586  subupgr  16636  uspgr2wlkeq  16728  clwwlkccatlem  16763  umgrclwwlkge2  16765  clwwlkn1loopb  16783  clwwlknonex2lem2  16801  eupth2lem3lem4fi  16836  eupth2fi  16842  2spim  16916  exmidcon  17159  alsralrex  17275