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  561  pm4.79dc  911  dedlema  978  dedlemb  979  19.35-1  1673  cbval2  1973  cbvex2  1974  nelelne  2506  r19.21be  2635  r19.35-1  2695  mosubt  2997  sbcrext  3123  uneqdifeqim  3599  ssuni  3941  uniss2  3950  elpwuni  4086  elssabg  4265  elpw2g  4273  epelg  4416  elomssom  4732  relop  4910  riinint  5023  cnviinm  5309  funopg  5391  fun  5541  tz6.12c  5705  fvelrnb  5729  fmptco  5848  funopsn  5865  fnressn  5875  fressnfv  5876  fvtp2g  5898  fvtp3g  5899  fconst2g  5904  isores3  5994  isoselem  5999  eloprabga  6148  fo1stresm  6368  poxp  6441  fsuppeq  6460  suppssdc  6473  brtpos2  6495  smores  6536  tfrlem1  6552  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  frecrdg  6652  oawordriexmid  6716  nnacl  6726  nnmcl  6727  nnacom  6730  nnaass  6731  nnmsucr  6734  nndifsnid  6753  nnmordi  6762  iinerm  6854  th3qlem2  6885  elpmg  6911  pmss12g  6922  mapsn  6938  brdomg  6998  f1domg  7010  ssdomg  7031  nndomo  7131  ffsuppbi  7266  elfi2  7272  nnnninfeq2  7433  carden2bex  7499  cc3  7598  addclpi  7658  addnidpig  7667  genpassl  7855  genpassu  7856  nqprloc  7876  ltaprlem  7949  recexprlemopl  7956  recexprlemopu  7958  recexprlemupu  7959  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemupu  7980  caucvgprlemupu  8003  caucvgprprlemupu  8031  archsr  8113  peano2nnnn  8184  receuap  8963  peano2nn  9269  nnaddcl  9277  zrevaddcl  9648  nzadd  9650  zdiv  9687  nneo  9702  zeo2  9705  peano5uzti  9707  fzind  9714  fnn0ind  9715  lbzbi  9969  qrevaddcl  9997  irradd  9999  irrmul  10000  ltsubrp  10044  ltaddrp  10045  xnn0xadd0  10222  icoshft  10345  fzen  10400  elfzm11  10450  uzsplit  10451  fzoval  10507  elfzom1elp1fzo  10572  exfzdc  10611  modaddmodup  10776  frec2uzrdg  10798  nninfinf  10832  seq3clss  10860  monoord  10874  seq3caopr3  10880  seqcaopr3g  10881  seq3f1olemp  10904  seqf1oglem2a  10907  seqf1og  10910  seq3id3  10913  seq3homo  10916  seq3z  10917  seqfeq4g  10920  ser3ge0  10925  expadd  10970  expmul  10973  leexp1a  10983  modqexp  11056  faccl  11125  facdiv  11128  faclbnd  11131  faclbnd6  11134  omgadd  11194  hashunsng  11200  hashmap  11220  seq3coll  11242  fundm2domnop0  11248  swrdswrdlem  11424  swrdswrd  11425  wrd2ind  11443  swrdccatin1  11445  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccat3  11454  shftlem  11529  resqrexlemover  11724  resqrexlemdecn  11726  resqrexlemlo  11727  resqrexlemcalc3  11730  climub  12058  climserle  12059  fsumzcl2  12120  fsumsplitsnun  12134  fsum2d  12150  modfsummodlemstep  12172  fsumabs  12180  fsumiun  12192  bcxmas  12204  cvgratnnlemnexp  12239  cvgratnnlemmn  12240  prodfap0  12260  prodfrecap  12261  ntrivcvgap  12263  prodmodc  12293  fprodssdc  12305  fprodabs  12331  fprod2d  12338  dvdsmod0  12508  dvds2ln  12539  dvdsabseq  12562  dvdsdivcl  12565  alzdvds  12569  oddnn02np1  12595  m1exp1  12616  nn0o1gt2  12620  nno  12621  ndvdsadd  12646  flodddiv4  12651  bitsinv1  12677  gcddiv  12744  gcdmultiple  12745  gcdmultiplez  12746  rplpwr  12752  dvdssq  12756  nninfct  12766  nn0seqcvgd  12767  alginv  12773  algcvga  12777  algfx  12778  isprm2  12843  isprm3  12844  prmdvdsexp  12874  eulerthlemrprm  12955  eulerthlema  12956  pcmpt  13070  ennnfoneleminc  13250  ennnfonelemkh  13251  ennnfonelemhf1o  13252  ennnfonelemhom  13254  omiunct  13283  nninfdclemlt  13290  setsn0fun  13337  mgmcl  13626  dfgrp3mlem  13857  mhmmulg  13920  resghm2b  14019  gsumfzconst  14098  srgpcomp  14237  lmodfopnelem1  14602  rmodislmodlem  14628  lss1d  14661  cnfldmulg  14854  cnfldexp  14855  gsumfzfsumlemm  14865  restopnb  15176  restdis  15179  tgcnp  15204  cnntr  15220  cnsscnp  15224  txcn  15270  txlm  15274  mettri  15368  blssexps  15424  blssex  15425  mopni3  15479  metss  15489  dvmptfsum  15720  plycolemc  15753  rpcxpmul2  15908  gausslemma2dlem6  16070  lgsquad2lem2  16085  2lgslem1c  16093  2lgslem3  16104  2lgs  16107  uhgredgrnv  16263  usgruspgrben  16311  usgredg2vlem2  16348  subupgr  16398  uspgr2wlkeq  16490  clwwlkccatlem  16525  umgrclwwlkge2  16527  clwwlkn1loopb  16545  clwwlknonex2lem2  16563  eupth2lem3lem4fi  16598  eupth2fi  16604  2spim  16678  exmidcon  16920