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 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  565  pm4.79dc  915  dedlema  982  dedlemb  983  19.35-1  1677  cbval2  1977  cbvex2  1978  nelelne  2512  r19.21be  2641  r19.35-1  2701  mosubt  3003  sbcrext  3129  uneqdifeqim  3613  ssuni  3957  uniss2  3966  elpwuni  4102  elssabg  4286  elpw2g  4294  epelg  4437  elomssom  4754  relop  4932  riinint  5045  cnviinm  5332  funopg  5414  fun  5564  tz6.12c  5728  fvelrnb  5753  fmptco  5877  funopsn  5894  fnressn  5904  fressnfv  5905  fvtp2g  5927  fvtp3g  5928  fconst2g  5933  isores3  6024  isoselem  6029  eloprabga  6178  fo1stresm  6399  poxp  6472  fsuppeq  6491  suppssdc  6504  brtpos2  6527  smores  6568  tfrlem1  6584  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  frecrdg  6684  oawordriexmid  6748  nnacl  6758  nnmcl  6759  nnacom  6762  nnaass  6763  nnmsucr  6766  nndifsnid  6785  nnmordi  6794  iinerm  6886  th3qlem2  6917  elpmg  6943  pmss12g  6961  mapsn  6978  brdomg  7038  f1domg  7050  ssdomg  7071  nndomo  7171  elfi2  7312  nnnninfeq2  7476  carden2bex  7542  cc3  7641  addclpi  7701  addnidpig  7710  genpassl  7898  genpassu  7899  nqprloc  7919  ltaprlem  7992  recexprlemopl  7999  recexprlemopu  8001  recexprlemupu  8002  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemupu  8023  caucvgprlemupu  8046  caucvgprprlemupu  8074  archsr  8156  peano2nnnn  8227  receuap  9008  indval0  9307  peano2nn  9326  nnaddcl  9334  zrevaddcl  9705  nzadd  9707  zdiv  9745  nneo  9760  zeo2  9763  peano5uzti  9765  fzind  9772  fnn0ind  9773  lbzbi  10032  qrevaddcl  10060  irradd  10062  irrmul  10064  ltsubrp  10108  ltaddrp  10109  xnn0xadd0  10286  icoshft  10409  fzen  10464  elfzm11  10515  uzsplit  10516  fzoval  10572  elfzom1elp1fzo  10637  exfzdc  10676  modaddmodup  10845  frec2uzrdg  10867  nninfinf  10901  seq3clss  10929  monoord  10943  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemp  10973  seqf1oglem2a  10976  seqf1og  10979  seq3id3  10982  seq3homo  10985  seq3z  10986  seqfeq4g  10989  ser3ge0  10994  expadd  11039  expmul  11042  leexp1a  11052  modqexp  11125  faccl  11195  facdiv  11198  faclbnd  11201  faclbnd6  11204  omgadd  11264  hashunsng  11270  hashmap  11290  hashf1  11309  seq3coll  11316  fundm2domnop0  11322  swrdswrdlem  11498  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccat3  11528  shftlem  11603  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc3  11804  climub  12135  climserle  12136  fsumzcl2  12197  fsumsplitsnun  12211  fsum2d  12227  modfsummodlemstep  12249  fsumabs  12257  fsumiun  12269  bcxmas  12281  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  prodfap0  12337  prodfrecap  12338  ntrivcvgap  12340  prodmodc  12370  fprodssdc  12382  fprodabs  12408  fprod2d  12415  dvdsmod0  12585  dvds2ln  12616  dvdsabseq  12639  dvdsdivcl  12642  alzdvds  12646  oddnn02np1  12672  m1exp1  12693  nn0o1gt2  12697  nno  12698  ndvdsadd  12723  flodddiv4  12728  bitsinv1  12754  gcddiv  12821  gcdmultiple  12822  gcdmultiplez  12823  rplpwr  12829  dvdssq  12833  nninfct  12843  nn0seqcvgd  12844  alginv  12850  algcvga  12854  algfx  12855  isprm2  12920  isprm3  12921  prmdvdsexp  12952  eulerthlemrprm  13036  eulerthlema  13037  pcmpt  13151  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  omiunct  13393  nninfdclemlt  13400  setsn0fun  13447  mgmcl  13738  dfgrp3mlem  13962  mhmmulg  14025  resghm2b  14124  cntzval  14153  gzsumconst  14233  srgpcomp  14401  lmodfopnelem1  14770  rmodislmodlem  14796  lss1d  14829  cnfldmulg  15022  cnfldexp  15023  restopnb  15440  restdis  15443  tgcnp  15468  cnntr  15484  cnsscnp  15488  txcn  15534  txlm  15538  mettri  15632  blssexps  15688  blssex  15689  mopni3  15743  metss  15753  dvmptfsum  15984  plycolemc  16017  rpcxpmul2  16179  ppiqub  16326  bcmono  16337  bpos1lem  16342  bposlem5  16348  gausslemma2dlem6  16424  lgsquad2lem2  16439  2lgslem1c  16447  2lgslem3  16458  2lgs  16461  uhgredgrnv  16617  usgruspgrben  16665  usgredg2vlem2  16702  subupgr  16752  uspgr2wlkeq  16844  clwwlkccatlem  16879  umgrclwwlkge2  16881  clwwlkn1loopb  16899  clwwlknonex2lem2  16917  eupth2lem3lem4fi  16952  eupth2fi  16958  2spim  17032  exmidcon  17275  alsralrex  17393