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  5433  tz6.12c  5591  fvelrnb  5611  fmptco  5731  fnressn  5751  fressnfv  5752  fvtp2g  5774  fvtp3g  5775  fconst2g  5780  isores3  5865  isoselem  5870  eloprabga  6013  fo1stresm  6228  poxp  6299  brtpos2  6318  smores  6359  tfrlem1  6375  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  frecrdg  6475  oawordriexmid  6537  nnacl  6547  nnmcl  6548  nnacom  6551  nnaass  6552  nnmsucr  6555  nndifsnid  6574  nnmordi  6583  iinerm  6675  th3qlem2  6706  elpmg  6732  pmss12g  6743  mapsn  6758  brdomg  6816  f1domg  6826  ssdomg  6846  nndomo  6934  elfi2  7047  nnnninfeq2  7204  carden2bex  7270  cc3  7353  addclpi  7413  addnidpig  7422  genpassl  7610  genpassu  7611  nqprloc  7631  ltaprlem  7704  recexprlemopl  7711  recexprlemopu  7713  recexprlemupu  7714  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemupu  7735  caucvgprlemupu  7758  caucvgprprlemupu  7786  archsr  7868  peano2nnnn  7939  receuap  8715  peano2nn  9021  nnaddcl  9029  zrevaddcl  9395  nzadd  9397  zdiv  9433  nneo  9448  zeo2  9451  peano5uzti  9453  fzind  9460  fnn0ind  9461  lbzbi  9709  qrevaddcl  9737  irradd  9739  irrmul  9740  ltsubrp  9784  ltaddrp  9785  xnn0xadd0  9961  icoshft  10084  fzen  10137  elfzm11  10185  uzsplit  10186  fzoval  10242  elfzom1elp1fzo  10297  exfzdc  10335  modaddmodup  10498  frec2uzrdg  10520  nninfinf  10554  seq3clss  10582  monoord  10596  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemp  10626  seqf1oglem2a  10629  seqf1og  10632  seq3id3  10635  seq3homo  10638  seq3z  10639  seqfeq4g  10642  ser3ge0  10647  expadd  10692  expmul  10695  leexp1a  10705  modqexp  10777  faccl  10846  facdiv  10849  faclbnd  10852  faclbnd6  10855  omgadd  10913  hashunsng  10918  seq3coll  10953  shftlem  11000  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc3  11200  climub  11528  climserle  11529  fsumzcl2  11589  fsumsplitsnun  11603  fsum2d  11619  modfsummodlemstep  11641  fsumabs  11649  fsumiun  11661  bcxmas  11673  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  prodfap0  11729  prodfrecap  11730  ntrivcvgap  11732  prodmodc  11762  fprodssdc  11774  fprodabs  11800  fprod2d  11807  dvdsmod0  11977  dvds2ln  12008  dvdsabseq  12031  dvdsdivcl  12034  alzdvds  12038  oddnn02np1  12064  m1exp1  12085  nn0o1gt2  12089  nno  12090  ndvdsadd  12115  flodddiv4  12120  bitsinv1  12146  gcddiv  12213  gcdmultiple  12214  gcdmultiplez  12215  rplpwr  12221  dvdssq  12225  nninfct  12235  nn0seqcvgd  12236  alginv  12242  algcvga  12246  algfx  12247  isprm2  12312  isprm3  12313  prmdvdsexp  12343  eulerthlemrprm  12424  eulerthlema  12425  pcmpt  12539  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemhom  12659  omiunct  12688  nninfdclemlt  12695  setsn0fun  12742  mgmcl  13063  dfgrp3mlem  13302  mhmmulg  13371  resghm2b  13470  gsumfzconst  13549  srgpcomp  13624  lmodfopnelem1  13958  rmodislmodlem  13984  lss1d  14017  cnfldmulg  14210  cnfldexp  14211  gsumfzfsumlemm  14221  restopnb  14525  restdis  14528  tgcnp  14553  cnntr  14569  cnsscnp  14573  txcn  14619  txlm  14623  mettri  14717  blssexps  14773  blssex  14774  mopni3  14828  metss  14838  dvmptfsum  15069  plycolemc  15102  rpcxpmul2  15257  gausslemma2dlem6  15416  lgsquad2lem2  15431  2lgslem1c  15439  2lgslem3  15450  2lgs  15453  2spim  15520