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  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  3955  uniss2  3964  elpwuni  4100  elssabg  4282  elpw2g  4290  epelg  4433  elomssom  4750  relop  4928  riinint  5041  cnviinm  5327  funopg  5409  fun  5559  tz6.12c  5723  fvelrnb  5747  fmptco  5868  funopsn  5885  fnressn  5895  fressnfv  5896  fvtp2g  5918  fvtp3g  5919  fconst2g  5924  isores3  6015  isoselem  6020  eloprabga  6169  fo1stresm  6389  poxp  6462  fsuppeq  6481  suppssdc  6494  brtpos2  6516  smores  6557  tfrlem1  6573  tfrlemi1  6597  tfr1onlemaccex  6613  tfrcllemaccex  6626  frecrdg  6673  oawordriexmid  6737  nnacl  6747  nnmcl  6748  nnacom  6751  nnaass  6752  nnmsucr  6755  nndifsnid  6774  nnmordi  6783  iinerm  6875  th3qlem2  6906  elpmg  6932  pmss12g  6950  mapsn  6966  brdomg  7026  f1domg  7038  ssdomg  7059  nndomo  7159  ffsuppbi  7294  elfi2  7300  nnnninfeq2  7463  carden2bex  7529  cc3  7628  addclpi  7688  addnidpig  7697  genpassl  7885  genpassu  7886  nqprloc  7906  ltaprlem  7979  recexprlemopl  7986  recexprlemopu  7988  recexprlemupu  7989  recexprlemss1l  7996  recexprlemss1u  7997  cauappcvgprlemupu  8010  caucvgprlemupu  8033  caucvgprprlemupu  8061  archsr  8143  peano2nnnn  8214  receuap  8993  peano2nn  9299  nnaddcl  9307  zrevaddcl  9678  nzadd  9680  zdiv  9717  nneo  9732  zeo2  9735  peano5uzti  9737  fzind  9744  fnn0ind  9745  lbzbi  9999  qrevaddcl  10027  irradd  10029  irrmul  10030  ltsubrp  10074  ltaddrp  10075  xnn0xadd0  10252  icoshft  10375  fzen  10430  elfzm11  10481  uzsplit  10482  fzoval  10538  elfzom1elp1fzo  10603  exfzdc  10642  modaddmodup  10807  frec2uzrdg  10829  nninfinf  10863  seq3clss  10891  monoord  10905  seq3caopr3  10911  seqcaopr3g  10912  seq3f1olemp  10935  seqf1oglem2a  10938  seqf1og  10941  seq3id3  10944  seq3homo  10947  seq3z  10948  seqfeq4g  10951  ser3ge0  10956  expadd  11001  expmul  11004  leexp1a  11014  modqexp  11087  faccl  11156  facdiv  11159  faclbnd  11162  faclbnd6  11165  omgadd  11225  hashunsng  11231  hashmap  11251  hashf1  11270  seq3coll  11277  fundm2domnop0  11283  swrdswrdlem  11459  swrdswrd  11460  wrd2ind  11478  swrdccatin1  11480  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccat3  11489  shftlem  11564  resqrexlemover  11759  resqrexlemdecn  11761  resqrexlemlo  11762  resqrexlemcalc3  11765  climub  12093  climserle  12094  fsumzcl2  12155  fsumsplitsnun  12169  fsum2d  12185  modfsummodlemstep  12207  fsumabs  12215  fsumiun  12227  bcxmas  12239  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  prodfap0  12295  prodfrecap  12296  ntrivcvgap  12298  prodmodc  12328  fprodssdc  12340  fprodabs  12366  fprod2d  12373  dvdsmod0  12543  dvds2ln  12574  dvdsabseq  12597  dvdsdivcl  12600  alzdvds  12604  oddnn02np1  12630  m1exp1  12651  nn0o1gt2  12655  nno  12656  ndvdsadd  12681  flodddiv4  12686  bitsinv1  12712  gcddiv  12779  gcdmultiple  12780  gcdmultiplez  12781  rplpwr  12787  dvdssq  12791  nninfct  12801  nn0seqcvgd  12802  alginv  12808  algcvga  12812  algfx  12813  isprm2  12878  isprm3  12879  prmdvdsexp  12909  eulerthlemrprm  12990  eulerthlema  12991  pcmpt  13105  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemhom  13289  omiunct  13318  nninfdclemlt  13325  setsn0fun  13372  mgmcl  13662  dfgrp3mlem  13886  mhmmulg  13949  resghm2b  14048  gzsumconst  14126  srgpcomp  14277  lmodfopnelem1  14644  rmodislmodlem  14670  lss1d  14703  cnfldmulg  14896  cnfldexp  14897  restopnb  15265  restdis  15268  tgcnp  15293  cnntr  15309  cnsscnp  15313  txcn  15359  txlm  15363  mettri  15457  blssexps  15513  blssex  15514  mopni3  15568  metss  15578  dvmptfsum  15809  plycolemc  15842  rpcxpmul2  15998  gausslemma2dlem6  16169  lgsquad2lem2  16184  2lgslem1c  16192  2lgslem3  16203  2lgs  16206  uhgredgrnv  16362  usgruspgrben  16410  usgredg2vlem2  16447  subupgr  16497  uspgr2wlkeq  16589  clwwlkccatlem  16624  umgrclwwlkge2  16626  clwwlkn1loopb  16644  clwwlknonex2lem2  16662  eupth2lem3lem4fi  16697  eupth2fi  16703  2spim  16777  exmidcon  17019  alsralrex  17127