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  4303  copsexg  4331  pocl  4395  pofun  4404  sowlin  4412  reusv1  4550  alxfr  4553  ralxfrALT  4559  iunpw  4572  onsucelsucr  4601  reg2exmidlema  4627  en2lp  4647  2optocl  4798  3optocl  4799  ssrel  4809  ssrel2  4811  ssrelrel  4821  relop  4875  xpidtr  5122  trin2  5123  poltletr  5132  xp11m  5170  relcnvtr  5251  iotaval  5293  funmo  5336  fundif  5368  fss  5488  f0dom0  5524  fv3  5655  tz6.12c  5662  mpteqb  5730  funfvima  5878  f1veqaeq  5902  isoselem  5953  oprabid  6042  ovg  6153  focdmex  6269  f1o2ndf1  6385  poxp  6389  tposfn2  6423  smoel  6457  tfri3  6524  nnaass  6644  nnmordi  6675  iinerm  6767  2ecoptocl  6783  3ecoptocl  6784  th3qlem2  6798  enm  6992  xpdom2  7003  xpf1o  7018  findcard2  7064  findcard2s  7065  eldju2ndl  7255  updjud  7265  nninfninc  7306  distrnq0  7662  addassnq0  7665  prcdnql  7687  prcunqu  7688  nn0ge2m1nn  9445  nn0le2is012  9545  fzind  9578  nn0ind-raph  9580  zindd  9581  uzin  9772  indstr  9805  xnn0xadd0  10080  icoshft  10203  fzen  10256  uzsubsubfz  10260  elfz1b  10303  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  elfzmlbp  10345  elfzodifsumelfzo  10424  ssfzo12bi  10448  elfzonelfzo  10453  modfzo0difsn  10634  frec2uzuzd  10641  expcllem  10789  mulexp  10817  leexp2r  10832  bernneq  10899  facdiv  10977  fundm2domnop0  11085  ccatsymb  11155  swrdnd  11212  swrdswrdlem  11257  swrdswrd  11258  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccat3  11287  swrdccat  11288  swrdccat3blem  11292  cjexp  11425  absexp  11611  clim2prod  12071  prodfap0  12077  prodfrecap  12078  prodmodc  12110  fprodabs  12148  addmodlteqALT  12391  oddge22np1  12413  nn0enne  12434  nn0o1gt2  12437  gcdneg  12524  dfgcd2  12556  rplpwr  12569  coprmdvds1  12634  qredeq  12639  cncongr1  12646  cncongr2  12647  prm2orodd  12669  nnnn0modprm0  12799  prm23lt5  12807  dvdsprmpweqnn  12880  dvdsprmpweqle  12881  oddprmdvds  12898  prmpwdvds  12899  setsn0fun  13090  isnmgm  13414  sgrpass  13462  insubm  13539  dfgrp3mlem  13652  fiinopn  14699  tgcl  14759  distop  14780  ssnei2  14852  tgcnp  14904  cnpnei  14914  cnmptcom  14993  neibl  15186  rpcxpmul2  15608  fsumdvdsmul  15686  zabsle1  15699  gausslemma2dlem1a  15758  gausslemma2dlem3  15763  lgsquad2lem2  15782  2lgs  15804  umgrnloop  15937  upgrpredgv  15965  upgredgpr  15968  wlkl1loop  16130  upgriswlkdc  16132  upgrwlkvtxedg  16136  uspgr2wlkeq  16137  wlkv0  16141  wlkres  16149  clwwlkccatlem  16169  loopclwwlkn1b  16187  umgr2cwwk2dif  16192  bj-nnbist  16217  sumdc2  16272