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  1592  19.33b2  1640  equtrr  1721  spimeh  1750  cbv1  1756  cbv1v  1758  equvini  1769  sbequ2  1780  ax11e  1807  ax11b  1837  sb6rf  1864  sb56  1897  exmoeudc  2105  moimv  2108  eupickbi  2124  exists2  2139  r19.12  2600  2gencl  2793  3gencl  2794  rspccv  2862  ceqex  2888  mo2icl  2940  mob  2943  euind  2948  reuind  2966  sseq2  3204  nelss  3241  difin  3397  reupick2  3446  uneqdifeqim  3533  difsn  3756  sssnm  3781  preq12b  3797  iinss2  3966  trintssm  4144  sspwb  4246  copsexg  4274  pocl  4335  pofun  4344  sowlin  4352  reusv1  4490  alxfr  4493  ralxfrALT  4499  iunpw  4512  onsucelsucr  4541  reg2exmidlema  4567  en2lp  4587  2optocl  4737  3optocl  4738  ssrel  4748  ssrel2  4750  ssrelrel  4760  relop  4813  xpidtr  5057  trin2  5058  poltletr  5067  xp11m  5105  relcnvtr  5186  iotaval  5227  funmo  5270  fss  5416  f0dom0  5448  fv3  5578  tz6.12c  5585  mpteqb  5649  funfvima  5791  f1veqaeq  5813  isoselem  5864  oprabid  5951  ovg  6059  focdmex  6169  f1o2ndf1  6283  poxp  6287  tposfn2  6321  smoel  6355  tfri3  6422  nnaass  6540  nnmordi  6571  iinerm  6663  2ecoptocl  6679  3ecoptocl  6680  th3qlem2  6694  enm  6876  xpdom2  6887  xpf1o  6902  findcard2  6947  findcard2s  6948  eldju2ndl  7133  updjud  7143  nninfninc  7184  distrnq0  7521  addassnq0  7524  prcdnql  7546  prcunqu  7547  nn0ge2m1nn  9303  nn0le2is012  9402  fzind  9435  nn0ind-raph  9437  zindd  9438  uzin  9628  indstr  9661  xnn0xadd0  9936  icoshft  10059  fzen  10112  uzsubsubfz  10116  elfz1b  10159  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  elfzmlbp  10201  elfzodifsumelfzo  10271  ssfzo12bi  10295  elfzonelfzo  10300  modfzo0difsn  10469  frec2uzuzd  10476  expcllem  10624  mulexp  10652  leexp2r  10667  bernneq  10734  facdiv  10812  cjexp  11040  absexp  11226  clim2prod  11685  prodfap0  11691  prodfrecap  11692  prodmodc  11724  fprodabs  11762  addmodlteqALT  12004  oddge22np1  12025  nn0enne  12046  nn0o1gt2  12049  gcdneg  12122  dfgcd2  12154  rplpwr  12167  coprmdvds1  12232  qredeq  12237  cncongr1  12244  cncongr2  12245  prm2orodd  12267  nnnn0modprm0  12396  prm23lt5  12404  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  oddprmdvds  12495  prmpwdvds  12496  setsn0fun  12658  isnmgm  12946  sgrpass  12994  insubm  13060  dfgrp3mlem  13173  fiinopn  14183  tgcl  14243  distop  14264  ssnei2  14336  tgcnp  14388  cnpnei  14398  cnmptcom  14477  neibl  14670  zabsle1  15156  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  lgsquad2lem2  15239  2lgs  15261  bj-nnbist  15306  sumdc2  15361