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  561  pm4.79dc  911  dedlema  978  dedlemb  979  19.35-1  1673  cbval2  1973  cbvex2  1974  nelelne  2506  r19.21be  2635  r19.35-1  2695  mosubt  2997  sbcrext  3123  uneqdifeqim  3599  ssuni  3941  uniss2  3950  elpwuni  4086  elssabg  4265  elpw2g  4273  epelg  4416  elomssom  4732  relop  4910  riinint  5023  cnviinm  5309  funopg  5391  fun  5541  tz6.12c  5705  fvelrnb  5729  fmptco  5848  funopsn  5865  fnressn  5875  fressnfv  5876  fvtp2g  5898  fvtp3g  5899  fconst2g  5904  isores3  5994  isoselem  5999  eloprabga  6148  fo1stresm  6368  poxp  6441  fsuppeq  6460  suppssdc  6473  brtpos2  6495  smores  6536  tfrlem1  6552  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  frecrdg  6652  oawordriexmid  6716  nnacl  6726  nnmcl  6727  nnacom  6730  nnaass  6731  nnmsucr  6734  nndifsnid  6753  nnmordi  6762  iinerm  6854  th3qlem2  6885  elpmg  6911  pmss12g  6922  mapsn  6938  brdomg  6998  f1domg  7010  ssdomg  7031  nndomo  7131  ffsuppbi  7266  elfi2  7272  nnnninfeq2  7433  carden2bex  7499  cc3  7598  addclpi  7658  addnidpig  7667  genpassl  7855  genpassu  7856  nqprloc  7876  ltaprlem  7949  recexprlemopl  7956  recexprlemopu  7958  recexprlemupu  7959  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemupu  7980  caucvgprlemupu  8003  caucvgprprlemupu  8031  archsr  8113  peano2nnnn  8184  receuap  8960  peano2nn  9266  nnaddcl  9274  zrevaddcl  9645  nzadd  9647  zdiv  9684  nneo  9699  zeo2  9702  peano5uzti  9704  fzind  9711  fnn0ind  9712  lbzbi  9966  qrevaddcl  9994  irradd  9996  irrmul  9997  ltsubrp  10041  ltaddrp  10042  xnn0xadd0  10219  icoshft  10342  fzen  10397  elfzm11  10447  uzsplit  10448  fzoval  10504  elfzom1elp1fzo  10569  exfzdc  10608  modaddmodup  10773  frec2uzrdg  10795  nninfinf  10829  seq3clss  10857  monoord  10871  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemp  10901  seqf1oglem2a  10904  seqf1og  10907  seq3id3  10910  seq3homo  10913  seq3z  10914  seqfeq4g  10917  ser3ge0  10922  expadd  10967  expmul  10970  leexp1a  10980  modqexp  11053  faccl  11122  facdiv  11125  faclbnd  11128  faclbnd6  11131  omgadd  11191  hashunsng  11197  hashmap  11217  seq3coll  11239  fundm2domnop0  11245  swrdswrdlem  11421  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccat3  11451  shftlem  11526  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc3  11726  climub  12054  climserle  12055  fsumzcl2  12116  fsumsplitsnun  12130  fsum2d  12146  modfsummodlemstep  12168  fsumabs  12176  fsumiun  12188  bcxmas  12200  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  prodfap0  12256  prodfrecap  12257  ntrivcvgap  12259  prodmodc  12289  fprodssdc  12301  fprodabs  12327  fprod2d  12334  dvdsmod0  12504  dvds2ln  12535  dvdsabseq  12558  dvdsdivcl  12561  alzdvds  12565  oddnn02np1  12591  m1exp1  12612  nn0o1gt2  12616  nno  12617  ndvdsadd  12642  flodddiv4  12647  bitsinv1  12673  gcddiv  12740  gcdmultiple  12741  gcdmultiplez  12742  rplpwr  12748  dvdssq  12752  nninfct  12762  nn0seqcvgd  12763  alginv  12769  algcvga  12773  algfx  12774  isprm2  12839  isprm3  12840  prmdvdsexp  12870  eulerthlemrprm  12951  eulerthlema  12952  pcmpt  13066  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemhom  13250  omiunct  13279  nninfdclemlt  13286  setsn0fun  13333  mgmcl  13656  dfgrp3mlem  13895  mhmmulg  13964  resghm2b  14063  gsumfzconst  14142  srgpcomp  14218  lmodfopnelem1  14584  rmodislmodlem  14610  lss1d  14643  cnfldmulg  14836  cnfldexp  14837  gsumfzfsumlemm  14847  restopnb  15158  restdis  15161  tgcnp  15186  cnntr  15202  cnsscnp  15206  txcn  15252  txlm  15256  mettri  15350  blssexps  15406  blssex  15407  mopni3  15461  metss  15471  dvmptfsum  15702  plycolemc  15735  rpcxpmul2  15890  gausslemma2dlem6  16052  lgsquad2lem2  16067  2lgslem1c  16075  2lgslem3  16086  2lgs  16089  uhgredgrnv  16245  usgruspgrben  16293  usgredg2vlem2  16330  subupgr  16380  uspgr2wlkeq  16472  clwwlkccatlem  16507  umgrclwwlkge2  16509  clwwlkn1loopb  16527  clwwlknonex2lem2  16545  eupth2lem3lem4fi  16580  eupth2fi  16586  2spim  16650  exmidcon  16892