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  2101  moimv  2104  eupickbi  2120  exists2  2135  r19.12  2596  2gencl  2785  3gencl  2786  rspccv  2853  ceqex  2879  mo2icl  2931  mob  2934  euind  2939  reuind  2957  sseq2  3194  nelss  3231  difin  3387  reupick2  3436  uneqdifeqim  3523  difsn  3744  sssnm  3769  preq12b  3785  iinss2  3954  trintssm  4132  sspwb  4234  copsexg  4262  pocl  4321  pofun  4330  sowlin  4338  reusv1  4476  alxfr  4479  ralxfrALT  4485  iunpw  4498  onsucelsucr  4525  reg2exmidlema  4551  en2lp  4571  2optocl  4721  3optocl  4722  ssrel  4732  ssrel2  4734  ssrelrel  4744  relop  4795  xpidtr  5037  trin2  5038  poltletr  5047  xp11m  5085  relcnvtr  5166  iotaval  5207  funmo  5250  fss  5396  f0dom0  5428  fv3  5557  tz6.12c  5564  mpteqb  5627  funfvima  5769  f1veqaeq  5791  isoselem  5842  oprabid  5928  ovg  6035  focdmex  6140  f1o2ndf1  6253  poxp  6257  tposfn2  6291  smoel  6325  tfri3  6392  nnaass  6510  nnmordi  6541  iinerm  6633  2ecoptocl  6649  3ecoptocl  6650  th3qlem2  6664  enm  6846  xpdom2  6857  xpf1o  6872  findcard2  6917  findcard2s  6918  eldju2ndl  7101  updjud  7111  distrnq0  7488  addassnq0  7491  prcdnql  7513  prcunqu  7514  nn0ge2m1nn  9266  nn0le2is012  9365  fzind  9398  nn0ind-raph  9400  zindd  9401  uzin  9590  indstr  9623  xnn0xadd0  9897  icoshft  10020  fzen  10073  uzsubsubfz  10077  elfz1b  10120  elfz0ubfz0  10155  elfz0fzfz0  10156  fz0fzelfz0  10157  elfzmlbp  10162  elfzodifsumelfzo  10231  ssfzo12bi  10255  elfzonelfzo  10260  modfzo0difsn  10426  frec2uzuzd  10433  expcllem  10562  mulexp  10590  leexp2r  10605  bernneq  10672  facdiv  10750  cjexp  10934  absexp  11120  clim2prod  11579  prodfap0  11585  prodfrecap  11586  prodmodc  11618  fprodabs  11656  addmodlteqALT  11897  oddge22np1  11918  nn0enne  11939  nn0o1gt2  11942  gcdneg  12015  dfgcd2  12047  rplpwr  12060  coprmdvds1  12123  qredeq  12128  cncongr1  12135  cncongr2  12136  prm2orodd  12158  nnnn0modprm0  12287  prm23lt5  12295  dvdsprmpweqnn  12368  dvdsprmpweqle  12369  oddprmdvds  12386  prmpwdvds  12387  setsn0fun  12549  isnmgm  12836  sgrpass  12871  insubm  12937  dfgrp3mlem  13042  fiinopn  13961  tgcl  14021  distop  14042  ssnei2  14114  tgcnp  14166  cnpnei  14176  cnmptcom  14255  neibl  14448  zabsle1  14858  bj-nnbist  14954  sumdc2  15009