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  903  dedlema  969  dedlemb  970  19.35-1  1624  cbval2  1921  cbvex2  1922  nelelne  2439  r19.21be  2568  r19.35-1  2627  mosubt  2916  sbcrext  3042  uneqdifeqim  3510  ssuni  3833  uniss2  3842  elpwuni  3978  elssabg  4150  elpw2g  4158  epelg  4292  elomssom  4606  relop  4779  riinint  4890  cnviinm  5172  funopg  5252  fun  5390  tz6.12c  5547  fvelrnb  5565  fmptco  5684  fnressn  5704  fressnfv  5705  fvtp2g  5727  fvtp3g  5728  fconst2g  5733  isores3  5818  isoselem  5823  eloprabga  5964  fo1stresm  6164  poxp  6235  brtpos2  6254  smores  6295  tfrlem1  6311  tfrlemi1  6335  tfr1onlemaccex  6351  tfrcllemaccex  6364  frecrdg  6411  oawordriexmid  6473  nnacl  6483  nnmcl  6484  nnacom  6487  nnaass  6488  nnmsucr  6491  nndifsnid  6510  nnmordi  6519  iinerm  6609  th3qlem2  6640  elpmg  6666  pmss12g  6677  mapsn  6692  brdomg  6750  f1domg  6760  ssdomg  6780  nndomo  6866  elfi2  6973  nnnninfeq2  7129  carden2bex  7190  cc3  7269  addclpi  7328  addnidpig  7337  genpassl  7525  genpassu  7526  nqprloc  7546  ltaprlem  7619  recexprlemopl  7626  recexprlemopu  7628  recexprlemupu  7629  recexprlemss1l  7636  recexprlemss1u  7637  cauappcvgprlemupu  7650  caucvgprlemupu  7673  caucvgprprlemupu  7701  archsr  7783  peano2nnnn  7854  receuap  8628  peano2nn  8933  nnaddcl  8941  zrevaddcl  9305  nzadd  9307  zdiv  9343  nneo  9358  zeo2  9361  peano5uzti  9363  fzind  9370  fnn0ind  9371  lbzbi  9618  qrevaddcl  9646  irradd  9648  irrmul  9649  ltsubrp  9692  ltaddrp  9693  xnn0xadd0  9869  icoshft  9992  fzen  10045  elfzm11  10093  uzsplit  10094  fzoval  10150  elfzom1elp1fzo  10204  exfzdc  10242  modaddmodup  10389  frec2uzrdg  10411  seq3clss  10469  monoord  10478  seq3caopr3  10483  seq3f1olemp  10504  seq3id3  10509  seq3homo  10512  seq3z  10513  ser3ge0  10519  expadd  10564  expmul  10567  leexp1a  10577  modqexp  10649  faccl  10717  facdiv  10720  faclbnd  10723  faclbnd6  10726  omgadd  10784  hashunsng  10789  seq3coll  10824  shftlem  10827  resqrexlemover  11021  resqrexlemdecn  11023  resqrexlemlo  11024  resqrexlemcalc3  11027  climub  11354  climserle  11355  fsumzcl2  11415  fsumsplitsnun  11429  fsum2d  11445  modfsummodlemstep  11467  fsumabs  11475  fsumiun  11487  bcxmas  11499  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  prodfap0  11555  prodfrecap  11556  ntrivcvgap  11558  prodmodc  11588  fprodssdc  11600  fprodabs  11626  fprod2d  11633  dvdsmod0  11802  dvds2ln  11833  dvdsabseq  11855  dvdsdivcl  11858  alzdvds  11862  oddnn02np1  11887  m1exp1  11908  nn0o1gt2  11912  nno  11913  ndvdsadd  11938  flodddiv4  11941  gcddiv  12022  gcdmultiple  12023  gcdmultiplez  12024  rplpwr  12030  dvdssq  12034  nn0seqcvgd  12043  alginv  12049  algcvga  12053  algfx  12054  isprm2  12119  isprm3  12120  prmdvdsexp  12150  eulerthlemrprm  12231  eulerthlema  12232  pcmpt  12343  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  omiunct  12447  nninfdclemlt  12454  setsn0fun  12501  mgmcl  12783  dfgrp3mlem  12973  mhmmulg  13029  srgpcomp  13178  lmodfopnelem1  13419  rmodislmodlem  13445  lss1d  13475  cnfldmulg  13509  cnfldexp  13510  restopnb  13720  restdis  13723  tgcnp  13748  cnntr  13764  cnsscnp  13768  txcn  13814  txlm  13818  mettri  13912  blssexps  13968  blssex  13969  mopni3  14023  metss  14033  2spim  14557