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  624  con3rr3  636  expt  661  mtt  689  jaod  722  orel1  730  pm2.62  753  pm2.64  806  pm2.75  814  pm2.61ddc  866  peircedc  919  dcbi  942  pm5.62dc  951  pm4.83dc  957  ccased  971  3impd  1245  3expd  1248  syldbl2  1326  mp3an1i  1364  pclem6  1416  simplbi2com  1487  19.21ht  1627  19.33b2  1675  equtrr  1756  spimeh  1785  cbv1  1791  cbv1v  1793  equvini  1804  sbequ2  1815  ax11e  1842  ax11b  1872  sb6rf  1899  sb56  1932  exmoeudc  2141  moimv  2144  eupickbi  2160  exists2  2175  r19.12  2637  2gencl  2834  3gencl  2835  vtocl4ga  2874  rspccv  2905  ceqex  2931  mo2icl  2983  mob  2986  euind  2991  reuind  3009  sseq2  3249  nelss  3286  difin  3442  reupick2  3491  uneqdifeqim  3578  difsn  3808  ssprsseq  3833  sssnm  3835  preq12b  3851  iinss2  4021  trintssm  4201  sspwb  4306  copsexg  4334  pocl  4398  pofun  4407  sowlin  4415  reusv1  4553  alxfr  4556  ralxfrALT  4562  iunpw  4575  onsucelsucr  4604  reg2exmidlema  4630  en2lp  4650  2optocl  4801  3optocl  4802  ssrel  4812  ssrel2  4814  ssrelrel  4824  relop  4878  xpidtr  5125  trin2  5126  poltletr  5135  xp11m  5173  relcnvtr  5254  iotaval  5296  funmo  5339  fundif  5371  fss  5491  f0dom0  5527  fv3  5658  tz6.12c  5665  mpteqb  5733  funfvima  5881  f1veqaeq  5905  isoselem  5956  oprabid  6045  ovg  6156  focdmex  6272  f1o2ndf1  6388  poxp  6392  tposfn2  6427  smoel  6461  tfri3  6528  nnaass  6648  nnmordi  6679  iinerm  6771  2ecoptocl  6787  3ecoptocl  6788  th3qlem2  6802  enm  6999  xpdom2  7010  xpf1o  7025  findcard2  7073  findcard2s  7074  eldju2ndl  7265  updjud  7275  nninfninc  7316  distrnq0  7672  addassnq0  7675  prcdnql  7697  prcunqu  7698  nn0ge2m1nn  9455  nn0le2is012  9555  fzind  9588  nn0ind-raph  9590  zindd  9591  uzin  9782  indstr  9820  xnn0xadd0  10095  icoshft  10218  fzen  10271  uzsubsubfz  10275  elfz1b  10318  elfz0ubfz0  10353  elfz0fzfz0  10354  fz0fzelfz0  10355  elfzmlbp  10360  elfzodifsumelfzo  10439  ssfzo12bi  10463  elfzonelfzo  10468  modfzo0difsn  10650  frec2uzuzd  10657  expcllem  10805  mulexp  10833  leexp2r  10848  bernneq  10915  facdiv  10993  fundm2domnop0  11102  ccatsymb  11172  swrdnd  11233  swrdswrdlem  11278  swrdswrd  11279  pfxccatin12lem2a  11301  pfxccatin12lem1  11302  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccat3  11308  swrdccat  11309  swrdccat3blem  11313  cjexp  11447  absexp  11633  clim2prod  12093  prodfap0  12099  prodfrecap  12100  prodmodc  12132  fprodabs  12170  addmodlteqALT  12413  oddge22np1  12435  nn0enne  12456  nn0o1gt2  12459  gcdneg  12546  dfgcd2  12578  rplpwr  12591  coprmdvds1  12656  qredeq  12661  cncongr1  12668  cncongr2  12669  prm2orodd  12691  nnnn0modprm0  12821  prm23lt5  12829  dvdsprmpweqnn  12902  dvdsprmpweqle  12903  oddprmdvds  12920  prmpwdvds  12921  setsn0fun  13112  isnmgm  13436  sgrpass  13484  insubm  13561  dfgrp3mlem  13674  fiinopn  14721  tgcl  14781  distop  14802  ssnei2  14874  tgcnp  14926  cnpnei  14936  cnmptcom  15015  neibl  15208  rpcxpmul2  15630  fsumdvdsmul  15708  zabsle1  15721  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  lgsquad2lem2  15804  2lgs  15826  umgrnloop  15960  upgrpredgv  15990  upgredgpr  15993  wlkl1loop  16169  upgriswlkdc  16171  upgrwlkvtxedg  16175  uspgr2wlkeq  16176  wlkv0  16180  wlkres  16188  clwwlkccatlem  16209  loopclwwlkn1b  16228  umgr2cwwk2dif  16233  clwwlknonex2lem2  16247  clwwlknonex2  16248  bj-nnbist  16290  sumdc2  16345