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  907  dedlema  974  dedlemb  975  19.35-1  1650  cbval2  1948  cbvex2  1949  nelelne  2472  r19.21be  2601  r19.35-1  2661  mosubt  2960  sbcrext  3086  uneqdifeqim  3557  ssuni  3889  uniss2  3898  elpwuni  4034  elssabg  4211  elpw2g  4219  epelg  4358  elomssom  4674  relop  4849  riinint  4961  cnviinm  5246  funopg  5328  fun  5473  tz6.12c  5633  fvelrnb  5654  fmptco  5774  funopsn  5790  fnressn  5798  fressnfv  5799  fvtp2g  5821  fvtp3g  5822  fconst2g  5827  isores3  5912  isoselem  5917  eloprabga  6062  fo1stresm  6277  poxp  6348  brtpos2  6367  smores  6408  tfrlem1  6424  tfrlemi1  6448  tfr1onlemaccex  6464  tfrcllemaccex  6477  frecrdg  6524  oawordriexmid  6586  nnacl  6596  nnmcl  6597  nnacom  6600  nnaass  6601  nnmsucr  6604  nndifsnid  6623  nnmordi  6632  iinerm  6724  th3qlem2  6755  elpmg  6781  pmss12g  6792  mapsn  6807  brdomg  6867  f1domg  6879  ssdomg  6900  nndomo  6993  elfi2  7107  nnnninfeq2  7264  carden2bex  7330  cc3  7422  addclpi  7482  addnidpig  7491  genpassl  7679  genpassu  7680  nqprloc  7700  ltaprlem  7773  recexprlemopl  7780  recexprlemopu  7782  recexprlemupu  7783  recexprlemss1l  7790  recexprlemss1u  7791  cauappcvgprlemupu  7804  caucvgprlemupu  7827  caucvgprprlemupu  7855  archsr  7937  peano2nnnn  8008  receuap  8784  peano2nn  9090  nnaddcl  9098  zrevaddcl  9465  nzadd  9467  zdiv  9503  nneo  9518  zeo2  9521  peano5uzti  9523  fzind  9530  fnn0ind  9531  lbzbi  9779  qrevaddcl  9807  irradd  9809  irrmul  9810  ltsubrp  9854  ltaddrp  9855  xnn0xadd0  10031  icoshft  10154  fzen  10207  elfzm11  10255  uzsplit  10256  fzoval  10312  elfzom1elp1fzo  10375  exfzdc  10413  modaddmodup  10576  frec2uzrdg  10598  nninfinf  10632  seq3clss  10660  monoord  10674  seq3caopr3  10680  seqcaopr3g  10681  seq3f1olemp  10704  seqf1oglem2a  10707  seqf1og  10710  seq3id3  10713  seq3homo  10716  seq3z  10717  seqfeq4g  10720  ser3ge0  10725  expadd  10770  expmul  10773  leexp1a  10783  modqexp  10855  faccl  10924  facdiv  10927  faclbnd  10930  faclbnd6  10933  omgadd  10991  hashunsng  10996  seq3coll  11031  fundm2domnop0  11034  swrdswrdlem  11202  swrdswrd  11203  wrd2ind  11221  swrdccatin1  11223  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccat3  11232  shftlem  11293  resqrexlemover  11487  resqrexlemdecn  11489  resqrexlemlo  11490  resqrexlemcalc3  11493  climub  11821  climserle  11822  fsumzcl2  11882  fsumsplitsnun  11896  fsum2d  11912  modfsummodlemstep  11934  fsumabs  11942  fsumiun  11954  bcxmas  11966  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  prodfap0  12022  prodfrecap  12023  ntrivcvgap  12025  prodmodc  12055  fprodssdc  12067  fprodabs  12093  fprod2d  12100  dvdsmod0  12270  dvds2ln  12301  dvdsabseq  12324  dvdsdivcl  12327  alzdvds  12331  oddnn02np1  12357  m1exp1  12378  nn0o1gt2  12382  nno  12383  ndvdsadd  12408  flodddiv4  12413  bitsinv1  12439  gcddiv  12506  gcdmultiple  12507  gcdmultiplez  12508  rplpwr  12514  dvdssq  12518  nninfct  12528  nn0seqcvgd  12529  alginv  12535  algcvga  12539  algfx  12540  isprm2  12605  isprm3  12606  prmdvdsexp  12636  eulerthlemrprm  12717  eulerthlema  12718  pcmpt  12832  ennnfoneleminc  12948  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemhom  12952  omiunct  12981  nninfdclemlt  12988  setsn0fun  13035  mgmcl  13358  dfgrp3mlem  13597  mhmmulg  13666  resghm2b  13765  gsumfzconst  13844  srgpcomp  13919  lmodfopnelem1  14253  rmodislmodlem  14279  lss1d  14312  cnfldmulg  14505  cnfldexp  14506  gsumfzfsumlemm  14516  restopnb  14820  restdis  14823  tgcnp  14848  cnntr  14864  cnsscnp  14868  txcn  14914  txlm  14918  mettri  15012  blssexps  15068  blssex  15069  mopni3  15123  metss  15133  dvmptfsum  15364  plycolemc  15397  rpcxpmul2  15552  gausslemma2dlem6  15711  lgsquad2lem2  15726  2lgslem1c  15734  2lgslem3  15745  2lgs  15748  uhgredgrnv  15901  usgruspgrben  15949  usgredg2vlem2  15986  2spim  16040