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  2981  sbcrext  3107  uneqdifeqim  3578  ssuni  3913  uniss2  3922  elpwuni  4058  elssabg  4236  elpw2g  4244  epelg  4385  elomssom  4701  relop  4878  riinint  4991  cnviinm  5276  funopg  5358  fun  5505  tz6.12c  5665  fvelrnb  5689  fmptco  5809  funopsn  5825  fnressn  5835  fressnfv  5836  fvtp2g  5858  fvtp3g  5859  fconst2g  5864  isores3  5951  isoselem  5956  eloprabga  6103  fo1stresm  6319  poxp  6392  brtpos2  6412  smores  6453  tfrlem1  6469  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  frecrdg  6569  oawordriexmid  6633  nnacl  6643  nnmcl  6644  nnacom  6647  nnaass  6648  nnmsucr  6651  nndifsnid  6670  nnmordi  6679  iinerm  6771  th3qlem2  6802  elpmg  6828  pmss12g  6839  mapsn  6854  brdomg  6914  f1domg  6926  ssdomg  6947  nndomo  7045  elfi2  7165  nnnninfeq2  7322  carden2bex  7388  cc3  7480  addclpi  7540  addnidpig  7549  genpassl  7737  genpassu  7738  nqprloc  7758  ltaprlem  7831  recexprlemopl  7838  recexprlemopu  7840  recexprlemupu  7841  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemupu  7862  caucvgprlemupu  7885  caucvgprprlemupu  7913  archsr  7995  peano2nnnn  8066  receuap  8842  peano2nn  9148  nnaddcl  9156  zrevaddcl  9523  nzadd  9525  zdiv  9561  nneo  9576  zeo2  9579  peano5uzti  9581  fzind  9588  fnn0ind  9589  lbzbi  9843  qrevaddcl  9871  irradd  9873  irrmul  9874  ltsubrp  9918  ltaddrp  9919  xnn0xadd0  10095  icoshft  10218  fzen  10271  elfzm11  10319  uzsplit  10320  fzoval  10376  elfzom1elp1fzo  10440  exfzdc  10479  modaddmodup  10642  frec2uzrdg  10664  nninfinf  10698  seq3clss  10726  monoord  10740  seq3caopr3  10746  seqcaopr3g  10747  seq3f1olemp  10770  seqf1oglem2a  10773  seqf1og  10776  seq3id3  10779  seq3homo  10782  seq3z  10783  seqfeq4g  10786  ser3ge0  10791  expadd  10836  expmul  10839  leexp1a  10849  modqexp  10921  faccl  10990  facdiv  10993  faclbnd  10996  faclbnd6  10999  omgadd  11058  hashunsng  11064  seq3coll  11099  fundm2domnop0  11102  swrdswrdlem  11278  swrdswrd  11279  wrd2ind  11297  swrdccatin1  11299  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccat3  11308  shftlem  11370  resqrexlemover  11564  resqrexlemdecn  11566  resqrexlemlo  11567  resqrexlemcalc3  11570  climub  11898  climserle  11899  fsumzcl2  11959  fsumsplitsnun  11973  fsum2d  11989  modfsummodlemstep  12011  fsumabs  12019  fsumiun  12031  bcxmas  12043  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  prodfap0  12099  prodfrecap  12100  ntrivcvgap  12102  prodmodc  12132  fprodssdc  12144  fprodabs  12170  fprod2d  12177  dvdsmod0  12347  dvds2ln  12378  dvdsabseq  12401  dvdsdivcl  12404  alzdvds  12408  oddnn02np1  12434  m1exp1  12455  nn0o1gt2  12459  nno  12460  ndvdsadd  12485  flodddiv4  12490  bitsinv1  12516  gcddiv  12583  gcdmultiple  12584  gcdmultiplez  12585  rplpwr  12591  dvdssq  12595  nninfct  12605  nn0seqcvgd  12606  alginv  12612  algcvga  12616  algfx  12617  isprm2  12682  isprm3  12683  prmdvdsexp  12713  eulerthlemrprm  12794  eulerthlema  12795  pcmpt  12909  ennnfoneleminc  13025  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemhom  13029  omiunct  13058  nninfdclemlt  13065  setsn0fun  13112  mgmcl  13435  dfgrp3mlem  13674  mhmmulg  13743  resghm2b  13842  gsumfzconst  13921  srgpcomp  13996  lmodfopnelem1  14331  rmodislmodlem  14357  lss1d  14390  cnfldmulg  14583  cnfldexp  14584  gsumfzfsumlemm  14594  restopnb  14898  restdis  14901  tgcnp  14926  cnntr  14942  cnsscnp  14946  txcn  14992  txlm  14996  mettri  15090  blssexps  15146  blssex  15147  mopni3  15201  metss  15211  dvmptfsum  15442  plycolemc  15475  rpcxpmul2  15630  gausslemma2dlem6  15789  lgsquad2lem2  15804  2lgslem1c  15812  2lgslem3  15823  2lgs  15826  uhgredgrnv  15982  usgruspgrben  16030  usgredg2vlem2  16067  uspgr2wlkeq  16176  clwwlkccatlem  16209  umgrclwwlkge2  16211  clwwlkn1loopb  16229  clwwlknonex2lem2  16247  2spim  16312