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 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  3702  difsn  3852  ssprsseq  3877  sssnm  3879  preq12b  3895  iinss2  4065  trintssm  4245  sspwb  4356  copsexg  4384  pocl  4448  pofun  4457  sowlin  4465  reusv1  4604  alxfr  4607  ralxfrALT  4613  iunpw  4626  onsucelsucr  4655  reg2exmidlema  4681  en2lp  4701  2optocl  4852  3optocl  4853  ssrel  4863  ssrel2  4865  ssrelrel  4875  relop  4930  xpidtr  5178  trin2  5179  poltletr  5188  xp11m  5226  relcnvtr  5307  iotaval  5349  funmo  5392  fundif  5425  fss  5546  f0dom0  5586  fv3  5718  tz6.12c  5725  mpteqb  5796  funfvima  5950  f1veqaeq  5975  isoselem  6026  oprabid  6117  ovg  6228  focdmex  6344  f1o2ndf1  6464  poxp  6468  tposfn2  6537  smoel  6571  tfri3  6638  nnaass  6758  nnmordi  6789  iinerm  6881  2ecoptocl  6897  3ecoptocl  6898  th3qlem2  6912  enm  7118  xpdom2  7129  xpf1o  7144  findcard2  7193  findcard2s  7194  suppeqfsuppbi  7295  eldju2ndl  7412  updjud  7422  nninfninc  7463  distrnq0  7826  addassnq0  7829  prcdnql  7851  prcunqu  7852  nn0ge2m1nn  9629  nn0le2is012  9730  fzind  9763  nn0ind-raph  9765  zindd  9766  uzin  9957  indstr  9995  xnn0xadd0  10271  icoshft  10394  fzen  10449  uzsubsubfz  10454  elfz1b  10499  elfz0ubfz0  10534  elfz0fzfz0  10535  fz0fzelfz0  10536  elfzmlbp  10541  elfzodifsumelfzo  10621  ssfzo12bi  10645  elfzonelfzo  10650  modfzo0difsn  10834  frec2uzuzd  10841  expcllem  10989  mulexp  11017  leexp2r  11032  bernneq  11100  facdiv  11178  fundm2domnop0  11302  ccatsymb  11372  swrdnd  11433  swrdswrdlem  11478  swrdswrd  11479  pfxccatin12lem2a  11501  pfxccatin12lem1  11502  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccat3  11508  swrdccat  11509  swrdccat3blem  11513  cjexp  11660  absexp  11847  clim2prod  12308  prodfap0  12314  prodfrecap  12315  prodmodc  12347  fprodabs  12385  addmodlteqALT  12628  oddge22np1  12650  nn0enne  12671  nn0o1gt2  12674  gcdneg  12761  dfgcd2  12793  rplpwr  12806  coprmdvds1  12871  qredeq  12876  cncongr1  12883  cncongr2  12884  prm2orodd  12906  nnnn0modprm0  13036  prm23lt5  13044  dvdsprmpweqnn  13117  dvdsprmpweqle  13118  oddprmdvds  13135  prmpwdvds  13136  setsn0fun  13391  isnmgm  13682  sgrpass  13725  insubm  13794  dfgrp3mlem  13905  fiinopn  15107  tgcl  15167  distop  15188  ssnei2  15260  tgcnp  15312  cnpnei  15322  cnmptcom  15401  neibl  15594  rpcxpmul2  16021  fsumdvdsmul  16111  zabsle1  16130  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  lgsquad2lem2  16213  2lgs  16235  umgrnloop  16369  upgrpredgv  16399  upgredgpr  16402  wlkl1loop  16611  upgriswlkdc  16613  upgrwlkvtxedg  16617  uspgr2wlkeq  16618  wlkv0  16622  wlkres  16632  clwwlkccatlem  16653  loopclwwlkn1b  16672  umgr2cwwk2dif  16677  clwwlknonex2lem2  16691  clwwlknonex2  16692  eupth2lem3lem4fi  16726  depindlem2  16760  bj-nnbist  16784  sumdc2  16839