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  905  dedlema  972  dedlemb  973  19.35-1  1648  cbval2  1946  cbvex2  1947  nelelne  2469  r19.21be  2598  r19.35-1  2657  mosubt  2951  sbcrext  3077  uneqdifeqim  3547  ssuni  3874  uniss2  3883  elpwuni  4019  elssabg  4196  elpw2g  4204  epelg  4341  elomssom  4657  relop  4832  riinint  4944  cnviinm  5229  funopg  5310  fun  5454  tz6.12c  5613  fvelrnb  5633  fmptco  5753  funopsn  5769  fnressn  5777  fressnfv  5778  fvtp2g  5800  fvtp3g  5801  fconst2g  5806  isores3  5891  isoselem  5896  eloprabga  6039  fo1stresm  6254  poxp  6325  brtpos2  6344  smores  6385  tfrlem1  6401  tfrlemi1  6425  tfr1onlemaccex  6441  tfrcllemaccex  6454  frecrdg  6501  oawordriexmid  6563  nnacl  6573  nnmcl  6574  nnacom  6577  nnaass  6578  nnmsucr  6581  nndifsnid  6600  nnmordi  6609  iinerm  6701  th3qlem2  6732  elpmg  6758  pmss12g  6769  mapsn  6784  brdomg  6844  f1domg  6856  ssdomg  6877  nndomo  6968  elfi2  7081  nnnninfeq2  7238  carden2bex  7304  cc3  7387  addclpi  7447  addnidpig  7456  genpassl  7644  genpassu  7645  nqprloc  7665  ltaprlem  7738  recexprlemopl  7745  recexprlemopu  7747  recexprlemupu  7748  recexprlemss1l  7755  recexprlemss1u  7756  cauappcvgprlemupu  7769  caucvgprlemupu  7792  caucvgprprlemupu  7820  archsr  7902  peano2nnnn  7973  receuap  8749  peano2nn  9055  nnaddcl  9063  zrevaddcl  9430  nzadd  9432  zdiv  9468  nneo  9483  zeo2  9486  peano5uzti  9488  fzind  9495  fnn0ind  9496  lbzbi  9744  qrevaddcl  9772  irradd  9774  irrmul  9775  ltsubrp  9819  ltaddrp  9820  xnn0xadd0  9996  icoshft  10119  fzen  10172  elfzm11  10220  uzsplit  10221  fzoval  10277  elfzom1elp1fzo  10338  exfzdc  10376  modaddmodup  10539  frec2uzrdg  10561  nninfinf  10595  seq3clss  10623  monoord  10637  seq3caopr3  10643  seqcaopr3g  10644  seq3f1olemp  10667  seqf1oglem2a  10670  seqf1og  10673  seq3id3  10676  seq3homo  10679  seq3z  10680  seqfeq4g  10683  ser3ge0  10688  expadd  10733  expmul  10736  leexp1a  10746  modqexp  10818  faccl  10887  facdiv  10890  faclbnd  10893  faclbnd6  10896  omgadd  10954  hashunsng  10959  seq3coll  10994  fundm2domnop0  10997  swrdswrdlem  11163  swrdswrd  11164  shftlem  11171  resqrexlemover  11365  resqrexlemdecn  11367  resqrexlemlo  11368  resqrexlemcalc3  11371  climub  11699  climserle  11700  fsumzcl2  11760  fsumsplitsnun  11774  fsum2d  11790  modfsummodlemstep  11812  fsumabs  11820  fsumiun  11832  bcxmas  11844  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  prodfap0  11900  prodfrecap  11901  ntrivcvgap  11903  prodmodc  11933  fprodssdc  11945  fprodabs  11971  fprod2d  11978  dvdsmod0  12148  dvds2ln  12179  dvdsabseq  12202  dvdsdivcl  12205  alzdvds  12209  oddnn02np1  12235  m1exp1  12256  nn0o1gt2  12260  nno  12261  ndvdsadd  12286  flodddiv4  12291  bitsinv1  12317  gcddiv  12384  gcdmultiple  12385  gcdmultiplez  12386  rplpwr  12392  dvdssq  12396  nninfct  12406  nn0seqcvgd  12407  alginv  12413  algcvga  12417  algfx  12418  isprm2  12483  isprm3  12484  prmdvdsexp  12514  eulerthlemrprm  12595  eulerthlema  12596  pcmpt  12710  ennnfoneleminc  12826  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemhom  12830  omiunct  12859  nninfdclemlt  12866  setsn0fun  12913  mgmcl  13235  dfgrp3mlem  13474  mhmmulg  13543  resghm2b  13642  gsumfzconst  13721  srgpcomp  13796  lmodfopnelem1  14130  rmodislmodlem  14156  lss1d  14189  cnfldmulg  14382  cnfldexp  14383  gsumfzfsumlemm  14393  restopnb  14697  restdis  14700  tgcnp  14725  cnntr  14741  cnsscnp  14745  txcn  14791  txlm  14795  mettri  14889  blssexps  14945  blssex  14946  mopni3  15000  metss  15010  dvmptfsum  15241  plycolemc  15274  rpcxpmul2  15429  gausslemma2dlem6  15588  lgsquad2lem2  15603  2lgslem1c  15611  2lgslem3  15622  2lgs  15625  2spim  15776