Theorem com12 30

Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
com12.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
com12	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 29	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl11  31  syl5  32  syl6com  35  mpcom  36  syli  37  syl2imc  39  pm2.27  40  syldc  46  pm2.43b  52  syl9r  73  com3r  79  pm2.86i  99  expcom  116  impcom  125  syl5ibcom  155  syl5ibrcom  157  pm5.501  244  impd  254  expd  258  pm3.21  264  imdistanri  446  pm2.24  622  con3rr3  634  expt  659  mtt  687  jaod  719  orel1  727  pm2.62  750  pm2.64  803  pm2.75  811  pm2.61ddc  863  peircedc  916  dcbi  939  pm5.62dc  948  pm4.83dc  954  ccased  968  3impd  1224  3expd  1227  syldbl2  1305  mp3an1i  1343  pclem6  1394  simplbi2com  1465  19.21ht  1605  19.33b2  1653  equtrr  1734  spimeh  1763  cbv1  1769  cbv1v  1771  equvini  1782  sbequ2  1793  ax11e  1820  ax11b  1850  sb6rf  1877  sb56  1910  exmoeudc  2118  moimv  2121  eupickbi  2137  exists2  2152  r19.12  2613  2gencl  2806  3gencl  2807  rspccv  2875  ceqex  2901  mo2icl  2953  mob  2956  euind  2961  reuind  2979  sseq2  3218  nelss  3255  difin  3411  reupick2  3460  uneqdifeqim  3547  difsn  3772  sssnm  3797  preq12b  3813  iinss2  3982  trintssm  4162  sspwb  4264  copsexg  4292  pocl  4354  pofun  4363  sowlin  4371  reusv1  4509  alxfr  4512  ralxfrALT  4518  iunpw  4531  onsucelsucr  4560  reg2exmidlema  4586  en2lp  4606  2optocl  4756  3optocl  4757  ssrel  4767  ssrel2  4769  ssrelrel  4779  relop  4832  xpidtr  5078  trin2  5079  poltletr  5088  xp11m  5126  relcnvtr  5207  iotaval  5248  funmo  5291  fundif  5323  fss  5443  f0dom0  5476  fv3  5606  tz6.12c  5613  mpteqb  5677  funfvima  5823  f1veqaeq  5845  isoselem  5896  oprabid  5983  ovg  6092  focdmex  6207  f1o2ndf1  6321  poxp  6325  tposfn2  6359  smoel  6393  tfri3  6460  nnaass  6578  nnmordi  6609  iinerm  6701  2ecoptocl  6717  3ecoptocl  6718  th3qlem2  6732  enm  6922  xpdom2  6933  xpf1o  6948  findcard2  6993  findcard2s  6994  eldju2ndl  7181  updjud  7191  nninfninc  7232  distrnq0  7579  addassnq0  7582  prcdnql  7604  prcunqu  7605  nn0ge2m1nn  9362  nn0le2is012  9462  fzind  9495  nn0ind-raph  9497  zindd  9498  uzin  9688  indstr  9721  xnn0xadd0  9996  icoshft  10119  fzen  10172  uzsubsubfz  10176  elfz1b  10219  elfz0ubfz0  10254  elfz0fzfz0  10255  fz0fzelfz0  10256  elfzmlbp  10261  elfzodifsumelfzo  10337  ssfzo12bi  10361  elfzonelfzo  10366  modfzo0difsn  10547  frec2uzuzd  10554  expcllem  10702  mulexp  10730  leexp2r  10745  bernneq  10812  facdiv  10890  fundm2domnop0  10997  ccatsymb  11066  swrdnd  11120  swrdswrdlem  11163  swrdswrd  11164  cjexp  11248  absexp  11434  clim2prod  11894  prodfap0  11900  prodfrecap  11901  prodmodc  11933  fprodabs  11971  addmodlteqALT  12214  oddge22np1  12236  nn0enne  12257  nn0o1gt2  12260  gcdneg  12347  dfgcd2  12379  rplpwr  12392  coprmdvds1  12457  qredeq  12462  cncongr1  12469  cncongr2  12470  prm2orodd  12492  nnnn0modprm0  12622  prm23lt5  12630  dvdsprmpweqnn  12703  dvdsprmpweqle  12704  oddprmdvds  12721  prmpwdvds  12722  setsn0fun  12913  isnmgm  13236  sgrpass  13284  insubm  13361  dfgrp3mlem  13474  fiinopn  14520  tgcl  14580  distop  14601  ssnei2  14673  tgcnp  14725  cnpnei  14735  cnmptcom  14814  neibl  15007  rpcxpmul2  15429  fsumdvdsmul  15507  zabsle1  15520  gausslemma2dlem1a  15579  gausslemma2dlem3  15584  lgsquad2lem2  15603  2lgs  15625  bj-nnbist  15754  sumdc2  15809