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  904  dedlema  971  dedlemb  972  19.35-1  1638  cbval2  1936  cbvex2  1937  nelelne  2459  r19.21be  2588  r19.35-1  2647  mosubt  2941  sbcrext  3067  uneqdifeqim  3537  ssuni  3862  uniss2  3871  elpwuni  4007  elssabg  4182  elpw2g  4190  epelg  4326  elomssom  4642  relop  4817  riinint  4928  cnviinm  5212  funopg  5293  fun  5431  tz6.12c  5589  fvelrnb  5609  fmptco  5729  fnressn  5749  fressnfv  5750  fvtp2g  5772  fvtp3g  5773  fconst2g  5778  isores3  5863  isoselem  5868  eloprabga  6010  fo1stresm  6220  poxp  6291  brtpos2  6310  smores  6351  tfrlem1  6367  tfrlemi1  6391  tfr1onlemaccex  6407  tfrcllemaccex  6420  frecrdg  6467  oawordriexmid  6529  nnacl  6539  nnmcl  6540  nnacom  6543  nnaass  6544  nnmsucr  6547  nndifsnid  6566  nnmordi  6575  iinerm  6667  th3qlem2  6698  elpmg  6724  pmss12g  6735  mapsn  6750  brdomg  6808  f1domg  6818  ssdomg  6838  nndomo  6926  elfi2  7039  nnnninfeq2  7196  carden2bex  7258  cc3  7337  addclpi  7396  addnidpig  7405  genpassl  7593  genpassu  7594  nqprloc  7614  ltaprlem  7687  recexprlemopl  7694  recexprlemopu  7696  recexprlemupu  7697  recexprlemss1l  7704  recexprlemss1u  7705  cauappcvgprlemupu  7718  caucvgprlemupu  7741  caucvgprprlemupu  7769  archsr  7851  peano2nnnn  7922  receuap  8698  peano2nn  9004  nnaddcl  9012  zrevaddcl  9378  nzadd  9380  zdiv  9416  nneo  9431  zeo2  9434  peano5uzti  9436  fzind  9443  fnn0ind  9444  lbzbi  9692  qrevaddcl  9720  irradd  9722  irrmul  9723  ltsubrp  9767  ltaddrp  9768  xnn0xadd0  9944  icoshft  10067  fzen  10120  elfzm11  10168  uzsplit  10169  fzoval  10225  elfzom1elp1fzo  10280  exfzdc  10318  modaddmodup  10481  frec2uzrdg  10503  nninfinf  10537  seq3clss  10565  monoord  10579  seq3caopr3  10585  seqcaopr3g  10586  seq3f1olemp  10609  seqf1oglem2a  10612  seqf1og  10615  seq3id3  10618  seq3homo  10621  seq3z  10622  seqfeq4g  10625  ser3ge0  10630  expadd  10675  expmul  10678  leexp1a  10688  modqexp  10760  faccl  10829  facdiv  10832  faclbnd  10835  faclbnd6  10838  omgadd  10896  hashunsng  10901  seq3coll  10936  shftlem  10983  resqrexlemover  11177  resqrexlemdecn  11179  resqrexlemlo  11180  resqrexlemcalc3  11183  climub  11511  climserle  11512  fsumzcl2  11572  fsumsplitsnun  11586  fsum2d  11602  modfsummodlemstep  11624  fsumabs  11632  fsumiun  11644  bcxmas  11656  cvgratnnlemnexp  11691  cvgratnnlemmn  11692  prodfap0  11712  prodfrecap  11713  ntrivcvgap  11715  prodmodc  11745  fprodssdc  11757  fprodabs  11783  fprod2d  11790  dvdsmod0  11960  dvds2ln  11991  dvdsabseq  12014  dvdsdivcl  12017  alzdvds  12021  oddnn02np1  12047  m1exp1  12068  nn0o1gt2  12072  nno  12073  ndvdsadd  12098  flodddiv4  12103  bitsinv1  12129  gcddiv  12196  gcdmultiple  12197  gcdmultiplez  12198  rplpwr  12204  dvdssq  12208  nninfct  12218  nn0seqcvgd  12219  alginv  12225  algcvga  12229  algfx  12230  isprm2  12295  isprm3  12296  prmdvdsexp  12326  eulerthlemrprm  12407  eulerthlema  12408  pcmpt  12522  ennnfoneleminc  12638  ennnfonelemkh  12639  ennnfonelemhf1o  12640  ennnfonelemhom  12642  omiunct  12671  nninfdclemlt  12678  setsn0fun  12725  mgmcl  13012  dfgrp3mlem  13240  mhmmulg  13303  resghm2b  13402  gsumfzconst  13481  srgpcomp  13556  lmodfopnelem1  13890  rmodislmodlem  13916  lss1d  13949  cnfldmulg  14142  cnfldexp  14143  gsumfzfsumlemm  14153  restopnb  14427  restdis  14430  tgcnp  14455  cnntr  14471  cnsscnp  14475  txcn  14521  txlm  14525  mettri  14619  blssexps  14675  blssex  14676  mopni3  14730  metss  14740  dvmptfsum  14971  plycolemc  15004  rpcxpmul2  15159  gausslemma2dlem6  15318  lgsquad2lem2  15333  2lgslem1c  15341  2lgslem3  15352  2lgs  15355  2spim  15422