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  692  jaod  725  orel1  733  pm2.62  756  pm2.64  809  pm2.75  817  pm2.61ddc  869  peircedc  922  dcbi  945  pm5.62dc  954  pm4.83dc  960  ccased  974  3impd  1248  3expd  1251  syldbl2  1329  mp3an1i  1367  pclem6  1419  simplbi2com  1490  19.21ht  1630  19.33b2  1678  equtrr  1758  spimeh  1788  cbv1  1794  cbv1v  1796  equvini  1807  sbequ2  1818  ax11e  1845  ax11b  1875  sb6rf  1902  sb56  1936  exmoeudc  2146  moimv  2149  eupickbi  2165  exists2  2180  r19.12  2651  2gencl  2849  3gencl  2850  vtocl4ga  2889  rspccv  2920  ceqex  2946  mo2icl  2998  mob  3001  euind  3006  reuind  3024  sseq2  3264  nelss  3301  difin  3460  reupick2  3509  uneqdifeqim  3597  sspw  3684  difsn  3833  ssprsseq  3858  sssnm  3860  preq12b  3876  iinss2  4046  trintssm  4226  sspwb  4334  copsexg  4362  pocl  4426  pofun  4435  sowlin  4443  reusv1  4581  alxfr  4584  ralxfrALT  4590  iunpw  4603  onsucelsucr  4632  reg2exmidlema  4658  en2lp  4678  2optocl  4829  3optocl  4830  ssrel  4840  ssrel2  4842  ssrelrel  4852  relop  4907  xpidtr  5155  trin2  5156  poltletr  5165  xp11m  5203  relcnvtr  5284  iotaval  5326  funmo  5369  fundif  5402  fss  5523  f0dom0  5563  fv3  5695  tz6.12c  5702  mpteqb  5770  funfvima  5920  f1veqaeq  5944  isoselem  5995  oprabid  6084  ovg  6195  focdmex  6310  f1o2ndf1  6426  poxp  6430  tposfn2  6499  smoel  6533  tfri3  6600  nnaass  6720  nnmordi  6751  iinerm  6843  2ecoptocl  6859  3ecoptocl  6860  th3qlem2  6874  enm  7073  xpdom2  7084  xpf1o  7099  findcard2  7148  findcard2s  7149  suppeqfsuppbi  7250  eldju2ndl  7365  updjud  7375  nninfninc  7416  distrnq0  7776  addassnq0  7779  prcdnql  7801  prcunqu  7802  nn0ge2m1nn  9562  nn0le2is012  9663  fzind  9696  nn0ind-raph  9698  zindd  9699  uzin  9890  indstr  9928  xnn0xadd0  10203  icoshft  10326  fzen  10380  uzsubsubfz  10384  elfz1b  10428  elfz0ubfz0  10463  elfz0fzfz0  10464  fz0fzelfz0  10465  elfzmlbp  10470  elfzodifsumelfzo  10550  ssfzo12bi  10574  elfzonelfzo  10579  modfzo0difsn  10761  frec2uzuzd  10768  expcllem  10916  mulexp  10944  leexp2r  10959  bernneq  11026  facdiv  11104  fundm2domnop0  11224  ccatsymb  11294  swrdnd  11355  swrdswrdlem  11400  swrdswrd  11401  pfxccatin12lem2a  11423  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccat3  11430  swrdccat  11431  swrdccat3blem  11435  cjexp  11582  absexp  11768  clim2prod  12229  prodfap0  12235  prodfrecap  12236  prodmodc  12268  fprodabs  12306  addmodlteqALT  12549  oddge22np1  12571  nn0enne  12592  nn0o1gt2  12595  gcdneg  12682  dfgcd2  12714  rplpwr  12727  coprmdvds1  12792  qredeq  12797  cncongr1  12804  cncongr2  12805  prm2orodd  12827  nnnn0modprm0  12957  prm23lt5  12965  dvdsprmpweqnn  13038  dvdsprmpweqle  13039  oddprmdvds  13056  prmpwdvds  13057  setsn0fun  13266  isnmgm  13590  sgrpass  13638  insubm  13715  dfgrp3mlem  13828  fiinopn  14886  tgcl  14946  distop  14967  ssnei2  15039  tgcnp  15091  cnpnei  15101  cnmptcom  15180  neibl  15373  rpcxpmul2  15795  fsumdvdsmul  15876  zabsle1  15889  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  lgsquad2lem2  15972  2lgs  15994  umgrnloop  16128  upgrpredgv  16158  upgredgpr  16161  wlkl1loop  16370  upgriswlkdc  16372  upgrwlkvtxedg  16376  uspgr2wlkeq  16377  wlkv0  16381  wlkres  16391  clwwlkccatlem  16412  loopclwwlkn1b  16431  umgr2cwwk2dif  16436  clwwlknonex2lem2  16450  clwwlknonex2  16451  eupth2lem3lem4fi  16485  depindlem2  16519  bj-nnbist  16533  sumdc2  16588