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  4286  elpw2g  4294  epelg  4437  elomssom  4754  relop  4932  riinint  5045  cnviinm  5332  funopg  5414  fun  5564  tz6.12c  5728  fvelrnb  5753  fmptco  5877  funopsn  5894  fnressn  5904  fressnfv  5905  fvtp2g  5927  fvtp3g  5928  fconst2g  5933  isores3  6024  isoselem  6029  eloprabga  6178  fo1stresm  6399  poxp  6472  fsuppeq  6491  suppssdc  6504  brtpos2  6526  smores  6567  tfrlem1  6583  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  frecrdg  6683  oawordriexmid  6747  nnacl  6757  nnmcl  6758  nnacom  6761  nnaass  6762  nnmsucr  6765  nndifsnid  6784  nnmordi  6793  iinerm  6885  th3qlem2  6916  elpmg  6942  pmss12g  6960  mapsn  6977  brdomg  7037  f1domg  7049  ssdomg  7070  nndomo  7170  ffsuppbi  7306  elfi2  7312  nnnninfeq2  7476  carden2bex  7542  cc3  7641  addclpi  7701  addnidpig  7710  genpassl  7898  genpassu  7899  nqprloc  7919  ltaprlem  7992  recexprlemopl  7999  recexprlemopu  8001  recexprlemupu  8002  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemupu  8023  caucvgprlemupu  8046  caucvgprprlemupu  8074  archsr  8156  peano2nnnn  8227  receuap  9008  indval0  9307  peano2nn  9326  nnaddcl  9334  zrevaddcl  9707  nzadd  9709  zdiv  9746  nneo  9761  zeo2  9764  peano5uzti  9766  fzind  9773  fnn0ind  9774  lbzbi  10033  qrevaddcl  10061  irradd  10063  irrmul  10065  ltsubrp  10109  ltaddrp  10110  xnn0xadd0  10287  icoshft  10410  fzen  10465  elfzm11  10516  uzsplit  10517  fzoval  10573  elfzom1elp1fzo  10638  exfzdc  10677  modaddmodup  10846  frec2uzrdg  10868  nninfinf  10902  seq3clss  10930  monoord  10944  seq3caopr3  10950  seqcaopr3g  10951  seq3f1olemp  10974  seqf1oglem2a  10977  seqf1og  10980  seq3id3  10983  seq3homo  10986  seq3z  10987  seqfeq4g  10990  ser3ge0  10995  expadd  11040  expmul  11043  leexp1a  11053  modqexp  11126  faccl  11196  facdiv  11199  faclbnd  11202  faclbnd6  11205  omgadd  11265  hashunsng  11271  hashmap  11291  hashf1  11310  seq3coll  11317  fundm2domnop0  11323  swrdswrdlem  11499  swrdswrd  11500  wrd2ind  11518  swrdccatin1  11520  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccat3  11529  shftlem  11604  resqrexlemover  11799  resqrexlemdecn  11801  resqrexlemlo  11802  resqrexlemcalc3  11805  climub  12136  climserle  12137  fsumzcl2  12198  fsumsplitsnun  12212  fsum2d  12228  modfsummodlemstep  12250  fsumabs  12258  fsumiun  12270  bcxmas  12282  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  prodfap0  12338  prodfrecap  12339  ntrivcvgap  12341  prodmodc  12371  fprodssdc  12383  fprodabs  12409  fprod2d  12416  dvdsmod0  12586  dvds2ln  12617  dvdsabseq  12640  dvdsdivcl  12643  alzdvds  12647  oddnn02np1  12673  m1exp1  12694  nn0o1gt2  12698  nno  12699  ndvdsadd  12724  flodddiv4  12729  bitsinv1  12755  gcddiv  12822  gcdmultiple  12823  gcdmultiplez  12824  rplpwr  12830  dvdssq  12834  nninfct  12844  nn0seqcvgd  12845  alginv  12851  algcvga  12855  algfx  12856  isprm2  12921  isprm3  12922  prmdvdsexp  12953  eulerthlemrprm  13037  eulerthlema  13038  pcmpt  13152  ennnfoneleminc  13361  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemhom  13365  omiunct  13394  nninfdclemlt  13401  setsn0fun  13448  mgmcl  13739  dfgrp3mlem  13963  mhmmulg  14026  resghm2b  14125  cntzval  14154  gzsumconst  14234  srgpcomp  14402  lmodfopnelem1  14771  rmodislmodlem  14797  lss1d  14830  cnfldmulg  15023  cnfldexp  15024  restopnb  15419  restdis  15422  tgcnp  15447  cnntr  15463  cnsscnp  15467  txcn  15513  txlm  15517  mettri  15611  blssexps  15667  blssex  15668  mopni3  15722  metss  15732  dvmptfsum  15963  plycolemc  15996  rpcxpmul2  16158  ppiqub  16305  bcmono  16316  bpos1lem  16321  bposlem5  16327  gausslemma2dlem6  16403  lgsquad2lem2  16418  2lgslem1c  16426  2lgslem3  16437  2lgs  16440  uhgredgrnv  16596  usgruspgrben  16644  usgredg2vlem2  16681  subupgr  16731  uspgr2wlkeq  16823  clwwlkccatlem  16858  umgrclwwlkge2  16860  clwwlkn1loopb  16878  clwwlknonex2lem2  16896  eupth2lem3lem4fi  16931  eupth2fi  16937  2spim  17011  exmidcon  17254  alsralrex  17372