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  559  pm4.79dc  908  dedlema  975  dedlemb  976  19.35-1  1670  cbval2  1968  cbvex2  1969  nelelne  2492  r19.21be  2621  r19.35-1  2681  mosubt  2980  sbcrext  3106  uneqdifeqim  3577  ssuni  3910  uniss2  3919  elpwuni  4055  elssabg  4233  elpw2g  4241  epelg  4382  elomssom  4698  relop  4875  riinint  4988  cnviinm  5273  funopg  5355  fun  5502  tz6.12c  5662  fvelrnb  5686  fmptco  5806  funopsn  5822  fnressn  5832  fressnfv  5833  fvtp2g  5855  fvtp3g  5856  fconst2g  5861  isores3  5948  isoselem  5953  eloprabga  6100  fo1stresm  6316  poxp  6389  brtpos2  6408  smores  6449  tfrlem1  6465  tfrlemi1  6489  tfr1onlemaccex  6505  tfrcllemaccex  6518  frecrdg  6565  oawordriexmid  6629  nnacl  6639  nnmcl  6640  nnacom  6643  nnaass  6644  nnmsucr  6647  nndifsnid  6666  nnmordi  6675  iinerm  6767  th3qlem2  6798  elpmg  6824  pmss12g  6835  mapsn  6850  brdomg  6910  f1domg  6922  ssdomg  6943  nndomo  7038  elfi2  7155  nnnninfeq2  7312  carden2bex  7378  cc3  7470  addclpi  7530  addnidpig  7539  genpassl  7727  genpassu  7728  nqprloc  7748  ltaprlem  7821  recexprlemopl  7828  recexprlemopu  7830  recexprlemupu  7831  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemupu  7852  caucvgprlemupu  7875  caucvgprprlemupu  7903  archsr  7985  peano2nnnn  8056  receuap  8832  peano2nn  9138  nnaddcl  9146  zrevaddcl  9513  nzadd  9515  zdiv  9551  nneo  9566  zeo2  9569  peano5uzti  9571  fzind  9578  fnn0ind  9579  lbzbi  9828  qrevaddcl  9856  irradd  9858  irrmul  9859  ltsubrp  9903  ltaddrp  9904  xnn0xadd0  10080  icoshft  10203  fzen  10256  elfzm11  10304  uzsplit  10305  fzoval  10361  elfzom1elp1fzo  10425  exfzdc  10463  modaddmodup  10626  frec2uzrdg  10648  nninfinf  10682  seq3clss  10710  monoord  10724  seq3caopr3  10730  seqcaopr3g  10731  seq3f1olemp  10754  seqf1oglem2a  10757  seqf1og  10760  seq3id3  10763  seq3homo  10766  seq3z  10767  seqfeq4g  10770  ser3ge0  10775  expadd  10820  expmul  10823  leexp1a  10833  modqexp  10905  faccl  10974  facdiv  10977  faclbnd  10980  faclbnd6  10983  omgadd  11041  hashunsng  11047  seq3coll  11082  fundm2domnop0  11085  swrdswrdlem  11257  swrdswrd  11258  wrd2ind  11276  swrdccatin1  11278  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccat3  11287  shftlem  11348  resqrexlemover  11542  resqrexlemdecn  11544  resqrexlemlo  11545  resqrexlemcalc3  11548  climub  11876  climserle  11877  fsumzcl2  11937  fsumsplitsnun  11951  fsum2d  11967  modfsummodlemstep  11989  fsumabs  11997  fsumiun  12009  bcxmas  12021  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  prodfap0  12077  prodfrecap  12078  ntrivcvgap  12080  prodmodc  12110  fprodssdc  12122  fprodabs  12148  fprod2d  12155  dvdsmod0  12325  dvds2ln  12356  dvdsabseq  12379  dvdsdivcl  12382  alzdvds  12386  oddnn02np1  12412  m1exp1  12433  nn0o1gt2  12437  nno  12438  ndvdsadd  12463  flodddiv4  12468  bitsinv1  12494  gcddiv  12561  gcdmultiple  12562  gcdmultiplez  12563  rplpwr  12569  dvdssq  12573  nninfct  12583  nn0seqcvgd  12584  alginv  12590  algcvga  12594  algfx  12595  isprm2  12660  isprm3  12661  prmdvdsexp  12691  eulerthlemrprm  12772  eulerthlema  12773  pcmpt  12887  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemhom  13007  omiunct  13036  nninfdclemlt  13043  setsn0fun  13090  mgmcl  13413  dfgrp3mlem  13652  mhmmulg  13721  resghm2b  13820  gsumfzconst  13899  srgpcomp  13974  lmodfopnelem1  14309  rmodislmodlem  14335  lss1d  14368  cnfldmulg  14561  cnfldexp  14562  gsumfzfsumlemm  14572  restopnb  14876  restdis  14879  tgcnp  14904  cnntr  14920  cnsscnp  14924  txcn  14970  txlm  14974  mettri  15068  blssexps  15124  blssex  15125  mopni3  15179  metss  15189  dvmptfsum  15420  plycolemc  15453  rpcxpmul2  15608  gausslemma2dlem6  15767  lgsquad2lem2  15782  2lgslem1c  15790  2lgslem3  15801  2lgs  15804  uhgredgrnv  15957  usgruspgrben  16005  usgredg2vlem2  16042  uspgr2wlkeq  16137  clwwlkccatlem  16169  umgrclwwlkge2  16171  clwwlkn1loopb  16188  2spim  16239