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  3536  ssuni  3861  uniss2  3870  elpwuni  4006  elssabg  4181  elpw2g  4189  epelg  4325  elomssom  4641  relop  4816  riinint  4927  cnviinm  5211  funopg  5292  fun  5430  tz6.12c  5588  fvelrnb  5608  fmptco  5728  fnressn  5748  fressnfv  5749  fvtp2g  5771  fvtp3g  5772  fconst2g  5777  isores3  5862  isoselem  5867  eloprabga  6009  fo1stresm  6219  poxp  6290  brtpos2  6309  smores  6350  tfrlem1  6366  tfrlemi1  6390  tfr1onlemaccex  6406  tfrcllemaccex  6419  frecrdg  6466  oawordriexmid  6528  nnacl  6538  nnmcl  6539  nnacom  6542  nnaass  6543  nnmsucr  6546  nndifsnid  6565  nnmordi  6574  iinerm  6666  th3qlem2  6697  elpmg  6723  pmss12g  6734  mapsn  6749  brdomg  6807  f1domg  6817  ssdomg  6837  nndomo  6925  elfi2  7038  nnnninfeq2  7195  carden2bex  7256  cc3  7335  addclpi  7394  addnidpig  7403  genpassl  7591  genpassu  7592  nqprloc  7612  ltaprlem  7685  recexprlemopl  7692  recexprlemopu  7694  recexprlemupu  7695  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemupu  7716  caucvgprlemupu  7739  caucvgprprlemupu  7767  archsr  7849  peano2nnnn  7920  receuap  8696  peano2nn  9002  nnaddcl  9010  zrevaddcl  9376  nzadd  9378  zdiv  9414  nneo  9429  zeo2  9432  peano5uzti  9434  fzind  9441  fnn0ind  9442  lbzbi  9690  qrevaddcl  9718  irradd  9720  irrmul  9721  ltsubrp  9765  ltaddrp  9766  xnn0xadd0  9942  icoshft  10065  fzen  10118  elfzm11  10166  uzsplit  10167  fzoval  10223  elfzom1elp1fzo  10278  exfzdc  10316  modaddmodup  10479  frec2uzrdg  10501  nninfinf  10535  seq3clss  10563  monoord  10577  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemp  10607  seqf1oglem2a  10610  seqf1og  10613  seq3id3  10616  seq3homo  10619  seq3z  10620  seqfeq4g  10623  ser3ge0  10628  expadd  10673  expmul  10676  leexp1a  10686  modqexp  10758  faccl  10827  facdiv  10830  faclbnd  10833  faclbnd6  10836  omgadd  10894  hashunsng  10899  seq3coll  10934  shftlem  10981  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc3  11181  climub  11509  climserle  11510  fsumzcl2  11570  fsumsplitsnun  11584  fsum2d  11600  modfsummodlemstep  11622  fsumabs  11630  fsumiun  11642  bcxmas  11654  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  prodfap0  11710  prodfrecap  11711  ntrivcvgap  11713  prodmodc  11743  fprodssdc  11755  fprodabs  11781  fprod2d  11788  dvdsmod0  11958  dvds2ln  11989  dvdsabseq  12012  dvdsdivcl  12015  alzdvds  12019  oddnn02np1  12045  m1exp1  12066  nn0o1gt2  12070  nno  12071  ndvdsadd  12096  flodddiv4  12101  gcddiv  12186  gcdmultiple  12187  gcdmultiplez  12188  rplpwr  12194  dvdssq  12198  nninfct  12208  nn0seqcvgd  12209  alginv  12215  algcvga  12219  algfx  12220  isprm2  12285  isprm3  12286  prmdvdsexp  12316  eulerthlemrprm  12397  eulerthlema  12398  pcmpt  12512  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemhom  12632  omiunct  12661  nninfdclemlt  12668  setsn0fun  12715  mgmcl  13002  dfgrp3mlem  13230  mhmmulg  13293  resghm2b  13392  gsumfzconst  13471  srgpcomp  13546  lmodfopnelem1  13880  rmodislmodlem  13906  lss1d  13939  cnfldmulg  14132  cnfldexp  14133  gsumfzfsumlemm  14143  restopnb  14417  restdis  14420  tgcnp  14445  cnntr  14461  cnsscnp  14465  txcn  14511  txlm  14515  mettri  14609  blssexps  14665  blssex  14666  mopni3  14720  metss  14730  dvmptfsum  14961  plycolemc  14994  rpcxpmul2  15149  gausslemma2dlem6  15308  lgsquad2lem2  15323  2lgslem1c  15331  2lgslem3  15342  2lgs  15345  2spim  15412