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  450  pm2.24  630  con3rr3  642  expt  667  mtt  696  jaod  729  orel1  737  pm2.62  760  pm2.64  813  pm2.75  821  pm2.61ddc  873  peircedc  926  dcbi  949  pm5.62dc  958  pm4.83dc  964  ccased  978  3impd  1252  3expd  1255  syldbl2  1333  mp3an1i  1371  pclem6  1423  simplbi2com  1494  19.21ht  1634  19.33b2  1682  equtrr  1762  spimeh  1792  cbv1  1798  cbv1v  1800  equvini  1811  sbequ2  1822  ax11e  1849  ax11b  1879  sb6rf  1906  sb56  1940  exmoeudc  2150  moimv  2153  eupickbi  2169  exists2  2184  r19.12  2657  2gencl  2855  3gencl  2856  vtocl4ga  2895  rspccv  2926  ceqex  2953  mo2icl  3005  mob  3008  euind  3013  reuind  3031  sseq2  3272  nelss  3309  difin  3468  reupick2  3519  uneqdifeqim  3613  sspw  3701  difsn  3850  ssprsseq  3875  sssnm  3877  preq12b  3893  iinss2  4063  trintssm  4243  sspwb  4354  copsexg  4382  pocl  4446  pofun  4455  sowlin  4463  reusv1  4602  alxfr  4605  ralxfrALT  4611  iunpw  4624  onsucelsucr  4653  reg2exmidlema  4679  en2lp  4699  2optocl  4850  3optocl  4851  ssrel  4861  ssrel2  4863  ssrelrel  4873  relop  4928  xpidtr  5176  trin2  5177  poltletr  5186  xp11m  5224  relcnvtr  5305  iotaval  5347  funmo  5390  fundif  5423  fss  5544  f0dom0  5584  fv3  5716  tz6.12c  5723  mpteqb  5793  funfvima  5944  f1veqaeq  5969  isoselem  6020  oprabid  6111  ovg  6222  focdmex  6338  f1o2ndf1  6458  poxp  6462  tposfn2  6531  smoel  6565  tfri3  6632  nnaass  6752  nnmordi  6783  iinerm  6875  2ecoptocl  6891  3ecoptocl  6892  th3qlem2  6906  enm  7112  xpdom2  7123  xpf1o  7138  findcard2  7187  findcard2s  7188  suppeqfsuppbi  7289  eldju2ndl  7406  updjud  7416  nninfninc  7457  distrnq0  7820  addassnq0  7823  prcdnql  7845  prcunqu  7846  nn0ge2m1nn  9610  nn0le2is012  9711  fzind  9744  nn0ind-raph  9746  zindd  9747  uzin  9938  indstr  9976  xnn0xadd0  10252  icoshft  10375  fzen  10430  uzsubsubfz  10435  elfz1b  10480  elfz0ubfz0  10515  elfz0fzfz0  10516  fz0fzelfz0  10517  elfzmlbp  10522  elfzodifsumelfzo  10602  ssfzo12bi  10626  elfzonelfzo  10631  modfzo0difsn  10815  frec2uzuzd  10822  expcllem  10970  mulexp  10998  leexp2r  11013  bernneq  11081  facdiv  11159  fundm2domnop0  11283  ccatsymb  11353  swrdnd  11414  swrdswrdlem  11459  swrdswrd  11460  pfxccatin12lem2a  11482  pfxccatin12lem1  11483  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccat3  11489  swrdccat  11490  swrdccat3blem  11494  cjexp  11641  absexp  11828  clim2prod  12289  prodfap0  12295  prodfrecap  12296  prodmodc  12328  fprodabs  12366  addmodlteqALT  12609  oddge22np1  12631  nn0enne  12652  nn0o1gt2  12655  gcdneg  12742  dfgcd2  12774  rplpwr  12787  coprmdvds1  12852  qredeq  12857  cncongr1  12864  cncongr2  12865  prm2orodd  12887  nnnn0modprm0  13017  prm23lt5  13025  dvdsprmpweqnn  13098  dvdsprmpweqle  13099  oddprmdvds  13116  prmpwdvds  13117  setsn0fun  13372  isnmgm  13663  sgrpass  13706  insubm  13775  dfgrp3mlem  13886  fiinopn  15088  tgcl  15148  distop  15169  ssnei2  15241  tgcnp  15293  cnpnei  15303  cnmptcom  15382  neibl  15575  rpcxpmul2  15998  fsumdvdsmul  16088  zabsle1  16101  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  lgsquad2lem2  16184  2lgs  16206  umgrnloop  16340  upgrpredgv  16370  upgredgpr  16373  wlkl1loop  16582  upgriswlkdc  16584  upgrwlkvtxedg  16588  uspgr2wlkeq  16589  wlkv0  16593  wlkres  16603  clwwlkccatlem  16624  loopclwwlkn1b  16643  umgr2cwwk2dif  16648  clwwlknonex2lem2  16662  clwwlknonex2  16663  eupth2lem3lem4fi  16697  depindlem2  16731  bj-nnbist  16755  sumdc2  16810