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  910  dedlema  977  dedlemb  978  19.35-1  1672  cbval2  1970  cbvex2  1971  nelelne  2494  r19.21be  2623  r19.35-1  2683  mosubt  2983  sbcrext  3109  uneqdifeqim  3580  ssuni  3915  uniss2  3924  elpwuni  4060  elssabg  4238  elpw2g  4246  epelg  4387  elomssom  4703  relop  4880  riinint  4993  cnviinm  5278  funopg  5360  fun  5508  tz6.12c  5669  fvelrnb  5693  fmptco  5813  funopsn  5830  fnressn  5840  fressnfv  5841  fvtp2g  5863  fvtp3g  5864  fconst2g  5869  isores3  5956  isoselem  5961  eloprabga  6108  fo1stresm  6324  poxp  6397  brtpos2  6417  smores  6458  tfrlem1  6474  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecrdg  6574  oawordriexmid  6638  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nnmsucr  6656  nndifsnid  6675  nnmordi  6684  iinerm  6776  th3qlem2  6807  elpmg  6833  pmss12g  6844  mapsn  6859  brdomg  6919  f1domg  6931  ssdomg  6952  nndomo  7050  elfi2  7171  nnnninfeq2  7328  carden2bex  7394  cc3  7487  addclpi  7547  addnidpig  7556  genpassl  7744  genpassu  7745  nqprloc  7765  ltaprlem  7838  recexprlemopl  7845  recexprlemopu  7847  recexprlemupu  7848  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemupu  7869  caucvgprlemupu  7892  caucvgprprlemupu  7920  archsr  8002  peano2nnnn  8073  receuap  8849  peano2nn  9155  nnaddcl  9163  zrevaddcl  9530  nzadd  9532  zdiv  9568  nneo  9583  zeo2  9586  peano5uzti  9588  fzind  9595  fnn0ind  9596  lbzbi  9850  qrevaddcl  9878  irradd  9880  irrmul  9881  ltsubrp  9925  ltaddrp  9926  xnn0xadd0  10102  icoshft  10225  fzen  10278  elfzm11  10326  uzsplit  10327  fzoval  10383  elfzom1elp1fzo  10448  exfzdc  10487  modaddmodup  10650  frec2uzrdg  10672  nninfinf  10706  seq3clss  10734  monoord  10748  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3homo  10790  seq3z  10791  seqfeq4g  10794  ser3ge0  10799  expadd  10844  expmul  10847  leexp1a  10857  modqexp  10929  faccl  10998  facdiv  11001  faclbnd  11004  faclbnd6  11007  omgadd  11066  hashunsng  11072  seq3coll  11107  fundm2domnop0  11110  swrdswrdlem  11286  swrdswrd  11287  wrd2ind  11305  swrdccatin1  11307  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccat3  11316  shftlem  11378  resqrexlemover  11572  resqrexlemdecn  11574  resqrexlemlo  11575  resqrexlemcalc3  11578  climub  11906  climserle  11907  fsumzcl2  11968  fsumsplitsnun  11982  fsum2d  11998  modfsummodlemstep  12020  fsumabs  12028  fsumiun  12040  bcxmas  12052  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  prodfap0  12108  prodfrecap  12109  ntrivcvgap  12111  prodmodc  12141  fprodssdc  12153  fprodabs  12179  fprod2d  12186  dvdsmod0  12356  dvds2ln  12387  dvdsabseq  12410  dvdsdivcl  12413  alzdvds  12417  oddnn02np1  12443  m1exp1  12464  nn0o1gt2  12468  nno  12469  ndvdsadd  12494  flodddiv4  12499  bitsinv1  12525  gcddiv  12592  gcdmultiple  12593  gcdmultiplez  12594  rplpwr  12600  dvdssq  12604  nninfct  12614  nn0seqcvgd  12615  alginv  12621  algcvga  12625  algfx  12626  isprm2  12691  isprm3  12692  prmdvdsexp  12722  eulerthlemrprm  12803  eulerthlema  12804  pcmpt  12918  ennnfoneleminc  13034  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemhom  13038  omiunct  13067  nninfdclemlt  13074  setsn0fun  13121  mgmcl  13444  dfgrp3mlem  13683  mhmmulg  13752  resghm2b  13851  gsumfzconst  13930  srgpcomp  14006  lmodfopnelem1  14341  rmodislmodlem  14367  lss1d  14400  cnfldmulg  14593  cnfldexp  14594  gsumfzfsumlemm  14604  restopnb  14908  restdis  14911  tgcnp  14936  cnntr  14952  cnsscnp  14956  txcn  15002  txlm  15006  mettri  15100  blssexps  15156  blssex  15157  mopni3  15211  metss  15221  dvmptfsum  15452  plycolemc  15485  rpcxpmul2  15640  gausslemma2dlem6  15799  lgsquad2lem2  15814  2lgslem1c  15822  2lgslem3  15833  2lgs  15836  uhgredgrnv  15992  usgruspgrben  16040  usgredg2vlem2  16077  subupgr  16127  uspgr2wlkeq  16219  clwwlkccatlem  16254  umgrclwwlkge2  16256  clwwlkn1loopb  16274  clwwlknonex2lem2  16292  eupth2lem3lem4fi  16327  eupth2fi  16333  2spim  16383