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  2980  sbcrext  3106  uneqdifeqim  3577  ssuni  3910  uniss2  3919  elpwuni  4055  elssabg  4232  elpw2g  4240  epelg  4381  elomssom  4697  relop  4872  riinint  4985  cnviinm  5270  funopg  5352  fun  5499  tz6.12c  5659  fvelrnb  5683  fmptco  5803  funopsn  5819  fnressn  5829  fressnfv  5830  fvtp2g  5852  fvtp3g  5853  fconst2g  5858  isores3  5945  isoselem  5950  eloprabga  6097  fo1stresm  6313  poxp  6384  brtpos2  6403  smores  6444  tfrlem1  6460  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecrdg  6560  oawordriexmid  6624  nnacl  6634  nnmcl  6635  nnacom  6638  nnaass  6639  nnmsucr  6642  nndifsnid  6661  nnmordi  6670  iinerm  6762  th3qlem2  6793  elpmg  6819  pmss12g  6830  mapsn  6845  brdomg  6905  f1domg  6917  ssdomg  6938  nndomo  7033  elfi2  7147  nnnninfeq2  7304  carden2bex  7370  cc3  7462  addclpi  7522  addnidpig  7531  genpassl  7719  genpassu  7720  nqprloc  7740  ltaprlem  7813  recexprlemopl  7820  recexprlemopu  7822  recexprlemupu  7823  recexprlemss1l  7830  recexprlemss1u  7831  cauappcvgprlemupu  7844  caucvgprlemupu  7867  caucvgprprlemupu  7895  archsr  7977  peano2nnnn  8048  receuap  8824  peano2nn  9130  nnaddcl  9138  zrevaddcl  9505  nzadd  9507  zdiv  9543  nneo  9558  zeo2  9561  peano5uzti  9563  fzind  9570  fnn0ind  9571  lbzbi  9819  qrevaddcl  9847  irradd  9849  irrmul  9850  ltsubrp  9894  ltaddrp  9895  xnn0xadd0  10071  icoshft  10194  fzen  10247  elfzm11  10295  uzsplit  10296  fzoval  10352  elfzom1elp1fzo  10416  exfzdc  10454  modaddmodup  10617  frec2uzrdg  10639  nninfinf  10673  seq3clss  10701  monoord  10715  seq3caopr3  10721  seqcaopr3g  10722  seq3f1olemp  10745  seqf1oglem2a  10748  seqf1og  10751  seq3id3  10754  seq3homo  10757  seq3z  10758  seqfeq4g  10761  ser3ge0  10766  expadd  10811  expmul  10814  leexp1a  10824  modqexp  10896  faccl  10965  facdiv  10968  faclbnd  10971  faclbnd6  10974  omgadd  11032  hashunsng  11037  seq3coll  11072  fundm2domnop0  11075  swrdswrdlem  11244  swrdswrd  11245  wrd2ind  11263  swrdccatin1  11265  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccat3  11274  shftlem  11335  resqrexlemover  11529  resqrexlemdecn  11531  resqrexlemlo  11532  resqrexlemcalc3  11535  climub  11863  climserle  11864  fsumzcl2  11924  fsumsplitsnun  11938  fsum2d  11954  modfsummodlemstep  11976  fsumabs  11984  fsumiun  11996  bcxmas  12008  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  prodfap0  12064  prodfrecap  12065  ntrivcvgap  12067  prodmodc  12097  fprodssdc  12109  fprodabs  12135  fprod2d  12142  dvdsmod0  12312  dvds2ln  12343  dvdsabseq  12366  dvdsdivcl  12369  alzdvds  12373  oddnn02np1  12399  m1exp1  12420  nn0o1gt2  12424  nno  12425  ndvdsadd  12450  flodddiv4  12455  bitsinv1  12481  gcddiv  12548  gcdmultiple  12549  gcdmultiplez  12550  rplpwr  12556  dvdssq  12560  nninfct  12570  nn0seqcvgd  12571  alginv  12577  algcvga  12581  algfx  12582  isprm2  12647  isprm3  12648  prmdvdsexp  12678  eulerthlemrprm  12759  eulerthlema  12760  pcmpt  12874  ennnfoneleminc  12990  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemhom  12994  omiunct  13023  nninfdclemlt  13030  setsn0fun  13077  mgmcl  13400  dfgrp3mlem  13639  mhmmulg  13708  resghm2b  13807  gsumfzconst  13886  srgpcomp  13961  lmodfopnelem1  14296  rmodislmodlem  14322  lss1d  14355  cnfldmulg  14548  cnfldexp  14549  gsumfzfsumlemm  14559  restopnb  14863  restdis  14866  tgcnp  14891  cnntr  14907  cnsscnp  14911  txcn  14957  txlm  14961  mettri  15055  blssexps  15111  blssex  15112  mopni3  15166  metss  15176  dvmptfsum  15407  plycolemc  15440  rpcxpmul2  15595  gausslemma2dlem6  15754  lgsquad2lem2  15769  2lgslem1c  15777  2lgslem3  15788  2lgs  15791  uhgredgrnv  15944  usgruspgrben  15992  usgredg2vlem2  16029  uspgr2wlkeq  16086  2spim  16154