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  626  con3rr3  638  expt  663  mtt  691  jaod  724  orel1  732  pm2.62  755  pm2.64  808  pm2.75  816  pm2.61ddc  868  peircedc  921  dcbi  944  pm5.62dc  953  pm4.83dc  959  ccased  973  3impd  1247  3expd  1250  syldbl2  1328  mp3an1i  1366  pclem6  1418  simplbi2com  1489  19.21ht  1629  19.33b2  1677  equtrr  1757  spimeh  1786  cbv1  1792  cbv1v  1794  equvini  1805  sbequ2  1816  ax11e  1843  ax11b  1873  sb6rf  1900  sb56  1933  exmoeudc  2142  moimv  2145  eupickbi  2161  exists2  2176  r19.12  2638  2gencl  2835  3gencl  2836  vtocl4ga  2875  rspccv  2906  ceqex  2932  mo2icl  2984  mob  2987  euind  2992  reuind  3010  sseq2  3250  nelss  3287  difin  3443  reupick2  3492  uneqdifeqim  3579  difsn  3811  ssprsseq  3836  sssnm  3838  preq12b  3854  iinss2  4024  trintssm  4204  sspwb  4310  copsexg  4338  pocl  4402  pofun  4411  sowlin  4419  reusv1  4557  alxfr  4560  ralxfrALT  4566  iunpw  4579  onsucelsucr  4608  reg2exmidlema  4634  en2lp  4654  2optocl  4805  3optocl  4806  ssrel  4816  ssrel2  4818  ssrelrel  4828  relop  4882  xpidtr  5129  trin2  5130  poltletr  5139  xp11m  5177  relcnvtr  5258  iotaval  5300  funmo  5343  fundif  5376  fss  5496  f0dom0  5533  fv3  5665  tz6.12c  5672  mpteqb  5740  funfvima  5891  f1veqaeq  5915  isoselem  5966  oprabid  6055  ovg  6166  focdmex  6282  f1o2ndf1  6398  poxp  6402  tposfn2  6437  smoel  6471  tfri3  6538  nnaass  6658  nnmordi  6689  iinerm  6781  2ecoptocl  6797  3ecoptocl  6798  th3qlem2  6812  enm  7009  xpdom2  7020  xpf1o  7035  findcard2  7083  findcard2s  7084  eldju2ndl  7276  updjud  7286  nninfninc  7327  distrnq0  7684  addassnq0  7687  prcdnql  7709  prcunqu  7710  nn0ge2m1nn  9467  nn0le2is012  9567  fzind  9600  nn0ind-raph  9602  zindd  9603  uzin  9794  indstr  9832  xnn0xadd0  10107  icoshft  10230  fzen  10283  uzsubsubfz  10287  elfz1b  10330  elfz0ubfz0  10365  elfz0fzfz0  10366  fz0fzelfz0  10367  elfzmlbp  10372  elfzodifsumelfzo  10452  ssfzo12bi  10476  elfzonelfzo  10481  modfzo0difsn  10663  frec2uzuzd  10670  expcllem  10818  mulexp  10846  leexp2r  10861  bernneq  10928  facdiv  11006  fundm2domnop0  11118  ccatsymb  11188  swrdnd  11249  swrdswrdlem  11294  swrdswrd  11295  pfxccatin12lem2a  11317  pfxccatin12lem1  11318  swrdccatin2  11319  pfxccatin12lem2  11321  pfxccatin12lem3  11322  pfxccat3  11324  swrdccat  11325  swrdccat3blem  11329  cjexp  11476  absexp  11662  clim2prod  12123  prodfap0  12129  prodfrecap  12130  prodmodc  12162  fprodabs  12200  addmodlteqALT  12443  oddge22np1  12465  nn0enne  12486  nn0o1gt2  12489  gcdneg  12576  dfgcd2  12608  rplpwr  12621  coprmdvds1  12686  qredeq  12691  cncongr1  12698  cncongr2  12699  prm2orodd  12721  nnnn0modprm0  12851  prm23lt5  12859  dvdsprmpweqnn  12932  dvdsprmpweqle  12933  oddprmdvds  12950  prmpwdvds  12951  setsn0fun  13142  isnmgm  13466  sgrpass  13514  insubm  13591  dfgrp3mlem  13704  fiinopn  14757  tgcl  14817  distop  14838  ssnei2  14910  tgcnp  14962  cnpnei  14972  cnmptcom  15051  neibl  15244  rpcxpmul2  15666  fsumdvdsmul  15744  zabsle1  15757  gausslemma2dlem1a  15816  gausslemma2dlem3  15821  lgsquad2lem2  15840  2lgs  15862  umgrnloop  15996  upgrpredgv  16026  upgredgpr  16029  wlkl1loop  16238  upgriswlkdc  16240  upgrwlkvtxedg  16244  uspgr2wlkeq  16245  wlkv0  16249  wlkres  16259  clwwlkccatlem  16280  loopclwwlkn1b  16299  umgr2cwwk2dif  16304  clwwlknonex2lem2  16318  clwwlknonex2  16319  eupth2lem3lem4fi  16353  depindlem2  16387  bj-nnbist  16401  sumdc2  16456