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  1635  cbval2  1933  cbvex2  1934  nelelne  2456  r19.21be  2585  r19.35-1  2644  mosubt  2937  sbcrext  3063  uneqdifeqim  3532  ssuni  3857  uniss2  3866  elpwuni  4002  elssabg  4177  elpw2g  4185  epelg  4321  elomssom  4637  relop  4812  riinint  4923  cnviinm  5207  funopg  5288  fun  5426  tz6.12c  5584  fvelrnb  5604  fmptco  5724  fnressn  5744  fressnfv  5745  fvtp2g  5767  fvtp3g  5768  fconst2g  5773  isores3  5858  isoselem  5863  eloprabga  6005  fo1stresm  6214  poxp  6285  brtpos2  6304  smores  6345  tfrlem1  6361  tfrlemi1  6385  tfr1onlemaccex  6401  tfrcllemaccex  6414  frecrdg  6461  oawordriexmid  6523  nnacl  6533  nnmcl  6534  nnacom  6537  nnaass  6538  nnmsucr  6541  nndifsnid  6560  nnmordi  6569  iinerm  6661  th3qlem2  6692  elpmg  6718  pmss12g  6729  mapsn  6744  brdomg  6802  f1domg  6812  ssdomg  6832  nndomo  6920  elfi2  7031  nnnninfeq2  7188  carden2bex  7249  cc3  7328  addclpi  7387  addnidpig  7396  genpassl  7584  genpassu  7585  nqprloc  7605  ltaprlem  7678  recexprlemopl  7685  recexprlemopu  7687  recexprlemupu  7688  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemupu  7709  caucvgprlemupu  7732  caucvgprprlemupu  7760  archsr  7842  peano2nnnn  7913  receuap  8688  peano2nn  8994  nnaddcl  9002  zrevaddcl  9367  nzadd  9369  zdiv  9405  nneo  9420  zeo2  9423  peano5uzti  9425  fzind  9432  fnn0ind  9433  lbzbi  9681  qrevaddcl  9709  irradd  9711  irrmul  9712  ltsubrp  9756  ltaddrp  9757  xnn0xadd0  9933  icoshft  10056  fzen  10109  elfzm11  10157  uzsplit  10158  fzoval  10214  elfzom1elp1fzo  10269  exfzdc  10307  modaddmodup  10458  frec2uzrdg  10480  nninfinf  10514  seq3clss  10542  monoord  10556  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemp  10586  seqf1oglem2a  10589  seqf1og  10592  seq3id3  10595  seq3homo  10598  seq3z  10599  seqfeq4g  10602  ser3ge0  10607  expadd  10652  expmul  10655  leexp1a  10665  modqexp  10737  faccl  10806  facdiv  10809  faclbnd  10812  faclbnd6  10815  omgadd  10873  hashunsng  10878  seq3coll  10913  shftlem  10960  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc3  11160  climub  11487  climserle  11488  fsumzcl2  11548  fsumsplitsnun  11562  fsum2d  11578  modfsummodlemstep  11600  fsumabs  11608  fsumiun  11620  bcxmas  11632  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  prodfap0  11688  prodfrecap  11689  ntrivcvgap  11691  prodmodc  11721  fprodssdc  11733  fprodabs  11759  fprod2d  11766  dvdsmod0  11936  dvds2ln  11967  dvdsabseq  11989  dvdsdivcl  11992  alzdvds  11996  oddnn02np1  12021  m1exp1  12042  nn0o1gt2  12046  nno  12047  ndvdsadd  12072  flodddiv4  12075  gcddiv  12156  gcdmultiple  12157  gcdmultiplez  12158  rplpwr  12164  dvdssq  12168  nninfct  12178  nn0seqcvgd  12179  alginv  12185  algcvga  12189  algfx  12190  isprm2  12255  isprm3  12256  prmdvdsexp  12286  eulerthlemrprm  12367  eulerthlema  12368  pcmpt  12481  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemhom  12572  omiunct  12601  nninfdclemlt  12608  setsn0fun  12655  mgmcl  12942  dfgrp3mlem  13170  mhmmulg  13233  resghm2b  13332  gsumfzconst  13411  srgpcomp  13486  lmodfopnelem1  13820  rmodislmodlem  13846  lss1d  13879  cnfldmulg  14064  cnfldexp  14065  gsumfzfsumlemm  14075  restopnb  14349  restdis  14352  tgcnp  14377  cnntr  14393  cnsscnp  14397  txcn  14443  txlm  14447  mettri  14541  blssexps  14597  blssex  14598  mopni3  14652  metss  14662  gausslemma2dlem6  15183  2spim  15258