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  2452  r19.21be  2581  r19.35-1  2640  mosubt  2929  sbcrext  3055  uneqdifeqim  3523  ssuni  3846  uniss2  3855  elpwuni  3991  elssabg  4166  elpw2g  4174  epelg  4308  elomssom  4622  relop  4795  riinint  4906  cnviinm  5188  funopg  5269  fun  5407  tz6.12c  5564  fvelrnb  5584  fmptco  5703  fnressn  5723  fressnfv  5724  fvtp2g  5746  fvtp3g  5747  fconst2g  5752  isores3  5837  isoselem  5842  eloprabga  5984  fo1stresm  6187  poxp  6258  brtpos2  6277  smores  6318  tfrlem1  6334  tfrlemi1  6358  tfr1onlemaccex  6374  tfrcllemaccex  6387  frecrdg  6434  oawordriexmid  6496  nnacl  6506  nnmcl  6507  nnacom  6510  nnaass  6511  nnmsucr  6514  nndifsnid  6533  nnmordi  6542  iinerm  6634  th3qlem2  6665  elpmg  6691  pmss12g  6702  mapsn  6717  brdomg  6775  f1domg  6785  ssdomg  6805  nndomo  6893  elfi2  7002  nnnninfeq2  7158  carden2bex  7219  cc3  7298  addclpi  7357  addnidpig  7366  genpassl  7554  genpassu  7555  nqprloc  7575  ltaprlem  7648  recexprlemopl  7655  recexprlemopu  7657  recexprlemupu  7658  recexprlemss1l  7665  recexprlemss1u  7666  cauappcvgprlemupu  7679  caucvgprlemupu  7702  caucvgprprlemupu  7730  archsr  7812  peano2nnnn  7883  receuap  8657  peano2nn  8962  nnaddcl  8970  zrevaddcl  9334  nzadd  9336  zdiv  9372  nneo  9387  zeo2  9390  peano5uzti  9392  fzind  9399  fnn0ind  9400  lbzbi  9648  qrevaddcl  9676  irradd  9678  irrmul  9679  ltsubrp  9722  ltaddrp  9723  xnn0xadd0  9899  icoshft  10022  fzen  10075  elfzm11  10123  uzsplit  10124  fzoval  10180  elfzom1elp1fzo  10234  exfzdc  10272  modaddmodup  10420  frec2uzrdg  10442  seq3clss  10500  monoord  10509  seq3caopr3  10514  seq3f1olemp  10535  seq3id3  10540  seq3homo  10543  seq3z  10544  seqfeq4g  10546  ser3ge0  10551  expadd  10596  expmul  10599  leexp1a  10609  modqexp  10681  faccl  10750  facdiv  10753  faclbnd  10756  faclbnd6  10759  omgadd  10817  hashunsng  10822  seq3coll  10857  shftlem  10860  resqrexlemover  11054  resqrexlemdecn  11056  resqrexlemlo  11057  resqrexlemcalc3  11060  climub  11387  climserle  11388  fsumzcl2  11448  fsumsplitsnun  11462  fsum2d  11478  modfsummodlemstep  11500  fsumabs  11508  fsumiun  11520  bcxmas  11532  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  prodfap0  11588  prodfrecap  11589  ntrivcvgap  11591  prodmodc  11621  fprodssdc  11633  fprodabs  11659  fprod2d  11666  dvdsmod0  11835  dvds2ln  11866  dvdsabseq  11888  dvdsdivcl  11891  alzdvds  11895  oddnn02np1  11920  m1exp1  11941  nn0o1gt2  11945  nno  11946  ndvdsadd  11971  flodddiv4  11974  gcddiv  12055  gcdmultiple  12056  gcdmultiplez  12057  rplpwr  12063  dvdssq  12067  nn0seqcvgd  12076  alginv  12082  algcvga  12086  algfx  12087  isprm2  12152  isprm3  12153  prmdvdsexp  12183  eulerthlemrprm  12264  eulerthlema  12265  pcmpt  12378  ennnfoneleminc  12465  ennnfonelemkh  12466  ennnfonelemhf1o  12467  ennnfonelemhom  12469  omiunct  12498  nninfdclemlt  12505  setsn0fun  12552  mgmcl  12838  dfgrp3mlem  13057  mhmmulg  13120  resghm2b  13218  srgpcomp  13361  lmodfopnelem1  13657  rmodislmodlem  13683  lss1d  13716  cnfldmulg  13896  cnfldexp  13897  restopnb  14158  restdis  14161  tgcnp  14186  cnntr  14202  cnsscnp  14206  txcn  14252  txlm  14256  mettri  14350  blssexps  14406  blssex  14407  mopni3  14461  metss  14471  2spim  14996