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  4247  sspwb  4358  copsexg  4386  pocl  4450  pofun  4459  sowlin  4467  reusv1  4606  alxfr  4609  ralxfrALT  4615  iunpw  4628  onsucelsucr  4657  reg2exmidlema  4683  en2lp  4703  2optocl  4854  3optocl  4855  ssrel  4865  ssrel2  4867  ssrelrel  4877  relop  4932  xpidtr  5181  trin2  5182  poltletr  5191  xp11m  5229  relcnvtr  5310  iotaval  5352  funmo  5395  fundif  5428  fss  5549  f0dom0  5589  fv3  5721  tz6.12c  5728  mpteqb  5799  funfvima  5953  f1veqaeq  5978  isoselem  6029  oprabid  6120  ovg  6231  focdmex  6348  f1o2ndf1  6468  poxp  6472  tposfn2  6541  smoel  6575  tfri3  6642  nnaass  6762  nnmordi  6793  iinerm  6885  2ecoptocl  6901  3ecoptocl  6902  th3qlem2  6916  enm  7123  xpdom2  7134  xpf1o  7149  findcard2  7198  findcard2s  7199  suppeqfsuppbi  7301  eldju2ndl  7419  updjud  7429  nninfninc  7470  distrnq0  7833  addassnq0  7836  prcdnql  7858  prcunqu  7859  nn0ge2m1nn  9639  nn0le2is012  9740  fzind  9773  nn0ind-raph  9775  zindd  9776  uzin  9972  indstr  10010  xnn0xadd0  10287  icoshft  10410  fzen  10465  uzsubsubfz  10470  elfz1b  10515  elfz0ubfz0  10550  elfz0fzfz0  10551  fz0fzelfz0  10552  elfzmlbp  10557  elfzodifsumelfzo  10637  ssfzo12bi  10661  elfzonelfzo  10666  modfzo0difsn  10854  frec2uzuzd  10861  expcllem  11009  mulexp  11037  leexp2r  11052  bernneq  11120  facdiv  11199  fundm2domnop0  11323  ccatsymb  11393  swrdnd  11454  swrdswrdlem  11499  swrdswrd  11500  pfxccatin12lem2a  11522  pfxccatin12lem1  11523  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12lem3  11527  pfxccat3  11529  swrdccat  11530  swrdccat3blem  11534  cjexp  11681  absexp  11869  clim2prod  12332  prodfap0  12338  prodfrecap  12339  prodmodc  12371  fprodabs  12409  addmodlteqALT  12652  oddge22np1  12674  nn0enne  12695  nn0o1gt2  12698  gcdneg  12785  dfgcd2  12817  rplpwr  12830  coprmdvds1  12895  qredeq  12900  cncongr1  12907  cncongr2  12908  prm2orodd  12930  nnnn0modprm0  13064  prm23lt5  13072  dvdsprmpweqnn  13145  dvdsprmpweqle  13146  oddprmdvds  13163  prmpwdvds  13164  setsn0fun  13448  isnmgm  13740  sgrpass  13783  insubm  13852  dfgrp3mlem  13963  fiinopn  15242  tgcl  15302  distop  15323  ssnei2  15395  tgcnp  15447  cnpnei  15457  cnmptcom  15536  neibl  15729  rpcxpmul2  16158  fsumdvdsmul  16297  zabsle1  16335  gausslemma2dlem1a  16394  gausslemma2dlem3  16399  lgsquad2lem2  16418  2lgs  16440  umgrnloop  16574  upgrpredgv  16604  upgredgpr  16607  wlkl1loop  16816  upgriswlkdc  16818  upgrwlkvtxedg  16822  uspgr2wlkeq  16823  wlkv0  16827  wlkres  16837  clwwlkccatlem  16858  loopclwwlkn1b  16877  umgr2cwwk2dif  16882  clwwlknonex2lem2  16896  clwwlknonex2  16897  eupth2lem3lem4fi  16931  depindlem2  16965  bj-nnbist  16989  sumdc2  17044