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  658  mtt  686  jaod  718  orel1  726  pm2.62  749  pm2.64  802  pm2.75  810  pm2.61ddc  862  peircedc  915  dcbi  938  pm5.62dc  947  pm4.83dc  953  ccased  967  3impd  1223  3expd  1226  mp3an1i  1341  pclem6  1385  simplbi2com  1455  19.21ht  1595  19.33b2  1643  equtrr  1724  spimeh  1753  cbv1  1759  cbv1v  1761  equvini  1772  sbequ2  1783  ax11e  1810  ax11b  1840  sb6rf  1867  sb56  1900  exmoeudc  2108  moimv  2111  eupickbi  2127  exists2  2142  r19.12  2603  2gencl  2796  3gencl  2797  rspccv  2865  ceqex  2891  mo2icl  2943  mob  2946  euind  2951  reuind  2969  sseq2  3208  nelss  3245  difin  3401  reupick2  3450  uneqdifeqim  3537  difsn  3760  sssnm  3785  preq12b  3801  iinss2  3970  trintssm  4148  sspwb  4250  copsexg  4278  pocl  4339  pofun  4348  sowlin  4356  reusv1  4494  alxfr  4497  ralxfrALT  4503  iunpw  4516  onsucelsucr  4545  reg2exmidlema  4571  en2lp  4591  2optocl  4741  3optocl  4742  ssrel  4752  ssrel2  4754  ssrelrel  4764  relop  4817  xpidtr  5061  trin2  5062  poltletr  5071  xp11m  5109  relcnvtr  5190  iotaval  5231  funmo  5274  fss  5422  f0dom0  5454  fv3  5584  tz6.12c  5591  mpteqb  5655  funfvima  5797  f1veqaeq  5819  isoselem  5870  oprabid  5957  ovg  6066  focdmex  6181  f1o2ndf1  6295  poxp  6299  tposfn2  6333  smoel  6367  tfri3  6434  nnaass  6552  nnmordi  6583  iinerm  6675  2ecoptocl  6691  3ecoptocl  6692  th3qlem2  6706  enm  6888  xpdom2  6899  xpf1o  6914  findcard2  6959  findcard2s  6960  eldju2ndl  7147  updjud  7157  nninfninc  7198  distrnq0  7545  addassnq0  7548  prcdnql  7570  prcunqu  7571  nn0ge2m1nn  9328  nn0le2is012  9427  fzind  9460  nn0ind-raph  9462  zindd  9463  uzin  9653  indstr  9686  xnn0xadd0  9961  icoshft  10084  fzen  10137  uzsubsubfz  10141  elfz1b  10184  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  elfzmlbp  10226  elfzodifsumelfzo  10296  ssfzo12bi  10320  elfzonelfzo  10325  modfzo0difsn  10506  frec2uzuzd  10513  expcllem  10661  mulexp  10689  leexp2r  10704  bernneq  10771  facdiv  10849  cjexp  11077  absexp  11263  clim2prod  11723  prodfap0  11729  prodfrecap  11730  prodmodc  11762  fprodabs  11800  addmodlteqALT  12043  oddge22np1  12065  nn0enne  12086  nn0o1gt2  12089  gcdneg  12176  dfgcd2  12208  rplpwr  12221  coprmdvds1  12286  qredeq  12291  cncongr1  12298  cncongr2  12299  prm2orodd  12321  nnnn0modprm0  12451  prm23lt5  12459  dvdsprmpweqnn  12532  dvdsprmpweqle  12533  oddprmdvds  12550  prmpwdvds  12551  setsn0fun  12742  isnmgm  13064  sgrpass  13112  insubm  13189  dfgrp3mlem  13302  fiinopn  14348  tgcl  14408  distop  14429  ssnei2  14501  tgcnp  14553  cnpnei  14563  cnmptcom  14642  neibl  14835  rpcxpmul2  15257  fsumdvdsmul  15335  zabsle1  15348  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  lgsquad2lem2  15431  2lgs  15453  bj-nnbist  15498  sumdc2  15553