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  2833  3gencl  2834  vtocl4ga  2873  rspccv  2904  ceqex  2930  mo2icl  2982  mob  2985  euind  2990  reuind  3008  sseq2  3248  nelss  3285  difin  3441  reupick2  3490  uneqdifeqim  3577  difsn  3805  ssprsseq  3830  sssnm  3832  preq12b  3848  iinss2  4018  trintssm  4198  sspwb  4302  copsexg  4330  pocl  4394  pofun  4403  sowlin  4411  reusv1  4549  alxfr  4552  ralxfrALT  4558  iunpw  4571  onsucelsucr  4600  reg2exmidlema  4626  en2lp  4646  2optocl  4796  3optocl  4797  ssrel  4807  ssrel2  4809  ssrelrel  4819  relop  4872  xpidtr  5119  trin2  5120  poltletr  5129  xp11m  5167  relcnvtr  5248  iotaval  5290  funmo  5333  fundif  5365  fss  5485  f0dom0  5521  fv3  5652  tz6.12c  5659  mpteqb  5727  funfvima  5875  f1veqaeq  5899  isoselem  5950  oprabid  6039  ovg  6150  focdmex  6266  f1o2ndf1  6380  poxp  6384  tposfn2  6418  smoel  6452  tfri3  6519  nnaass  6639  nnmordi  6670  iinerm  6762  2ecoptocl  6778  3ecoptocl  6779  th3qlem2  6793  enm  6987  xpdom2  6998  xpf1o  7013  findcard2  7059  findcard2s  7060  eldju2ndl  7247  updjud  7257  nninfninc  7298  distrnq0  7654  addassnq0  7657  prcdnql  7679  prcunqu  7680  nn0ge2m1nn  9437  nn0le2is012  9537  fzind  9570  nn0ind-raph  9572  zindd  9573  uzin  9763  indstr  9796  xnn0xadd0  10071  icoshft  10194  fzen  10247  uzsubsubfz  10251  elfz1b  10294  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  elfzmlbp  10336  elfzodifsumelfzo  10415  ssfzo12bi  10439  elfzonelfzo  10444  modfzo0difsn  10625  frec2uzuzd  10632  expcllem  10780  mulexp  10808  leexp2r  10823  bernneq  10890  facdiv  10968  fundm2domnop0  11075  ccatsymb  11145  swrdnd  11199  swrdswrdlem  11244  swrdswrd  11245  pfxccatin12lem2a  11267  pfxccatin12lem1  11268  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccat3  11274  swrdccat  11275  swrdccat3blem  11279  cjexp  11412  absexp  11598  clim2prod  12058  prodfap0  12064  prodfrecap  12065  prodmodc  12097  fprodabs  12135  addmodlteqALT  12378  oddge22np1  12400  nn0enne  12421  nn0o1gt2  12424  gcdneg  12511  dfgcd2  12543  rplpwr  12556  coprmdvds1  12621  qredeq  12626  cncongr1  12633  cncongr2  12634  prm2orodd  12656  nnnn0modprm0  12786  prm23lt5  12794  dvdsprmpweqnn  12867  dvdsprmpweqle  12868  oddprmdvds  12885  prmpwdvds  12886  setsn0fun  13077  isnmgm  13401  sgrpass  13449  insubm  13526  dfgrp3mlem  13639  fiinopn  14686  tgcl  14746  distop  14767  ssnei2  14839  tgcnp  14891  cnpnei  14901  cnmptcom  14980  neibl  15173  rpcxpmul2  15595  fsumdvdsmul  15673  zabsle1  15686  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  lgsquad2lem2  15769  2lgs  15791  umgrnloop  15924  upgrpredgv  15952  upgredgpr  15955  wlkl1loop  16079  upgriswlkdc  16081  upgrwlkvtxedg  16085  uspgr2wlkeq  16086  wlkv0  16090  wlkres  16098  bj-nnbist  16132  sumdc2  16187