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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
com12	|- ( ps -> ( ph -> ch ) )

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		com12.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5com 29	1 |- ( ps -> ( ph -> ch ) )

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  622  con3rr3  634  expt  659  mtt  687  jaod  719  orel1  727  pm2.62  750  pm2.64  803  pm2.75  811  pm2.61ddc  863  peircedc  916  dcbi  939  pm5.62dc  948  pm4.83dc  954  ccased  968  3impd  1224  3expd  1227  syldbl2  1305  mp3an1i  1343  pclem6  1394  simplbi2com  1465  19.21ht  1605  19.33b2  1653  equtrr  1734  spimeh  1763  cbv1  1769  cbv1v  1771  equvini  1782  sbequ2  1793  ax11e  1820  ax11b  1850  sb6rf  1877  sb56  1910  exmoeudc  2119  moimv  2122  eupickbi  2138  exists2  2153  r19.12  2614  2gencl  2810  3gencl  2811  vtocl4ga  2850  rspccv  2881  ceqex  2907  mo2icl  2959  mob  2962  euind  2967  reuind  2985  sseq2  3225  nelss  3262  difin  3418  reupick2  3467  uneqdifeqim  3554  difsn  3781  ssprsseq  3806  sssnm  3808  preq12b  3824  iinss2  3994  trintssm  4174  sspwb  4278  copsexg  4306  pocl  4368  pofun  4377  sowlin  4385  reusv1  4523  alxfr  4526  ralxfrALT  4532  iunpw  4545  onsucelsucr  4574  reg2exmidlema  4600  en2lp  4620  2optocl  4770  3optocl  4771  ssrel  4781  ssrel2  4783  ssrelrel  4793  relop  4846  xpidtr  5092  trin2  5093  poltletr  5102  xp11m  5140  relcnvtr  5221  iotaval  5262  funmo  5305  fundif  5337  fss  5457  f0dom0  5491  fv3  5622  tz6.12c  5629  mpteqb  5693  funfvima  5839  f1veqaeq  5861  isoselem  5912  oprabid  5999  ovg  6108  focdmex  6223  f1o2ndf1  6337  poxp  6341  tposfn2  6375  smoel  6409  tfri3  6476  nnaass  6594  nnmordi  6625  iinerm  6717  2ecoptocl  6733  3ecoptocl  6734  th3qlem2  6748  enm  6940  xpdom2  6951  xpf1o  6966  findcard2  7012  findcard2s  7013  eldju2ndl  7200  updjud  7210  nninfninc  7251  distrnq0  7607  addassnq0  7610  prcdnql  7632  prcunqu  7633  nn0ge2m1nn  9390  nn0le2is012  9490  fzind  9523  nn0ind-raph  9525  zindd  9526  uzin  9716  indstr  9749  xnn0xadd0  10024  icoshft  10147  fzen  10200  uzsubsubfz  10204  elfz1b  10247  elfz0ubfz0  10282  elfz0fzfz0  10283  fz0fzelfz0  10284  elfzmlbp  10289  elfzodifsumelfzo  10367  ssfzo12bi  10391  elfzonelfzo  10396  modfzo0difsn  10577  frec2uzuzd  10584  expcllem  10732  mulexp  10760  leexp2r  10775  bernneq  10842  facdiv  10920  fundm2domnop0  11027  ccatsymb  11096  swrdnd  11150  swrdswrdlem  11195  swrdswrd  11196  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  swrdccat3blem  11230  cjexp  11319  absexp  11505  clim2prod  11965  prodfap0  11971  prodfrecap  11972  prodmodc  12004  fprodabs  12042  addmodlteqALT  12285  oddge22np1  12307  nn0enne  12328  nn0o1gt2  12331  gcdneg  12418  dfgcd2  12450  rplpwr  12463  coprmdvds1  12528  qredeq  12533  cncongr1  12540  cncongr2  12541  prm2orodd  12563  nnnn0modprm0  12693  prm23lt5  12701  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  oddprmdvds  12792  prmpwdvds  12793  setsn0fun  12984  isnmgm  13307  sgrpass  13355  insubm  13432  dfgrp3mlem  13545  fiinopn  14591  tgcl  14651  distop  14672  ssnei2  14744  tgcnp  14796  cnpnei  14806  cnmptcom  14885  neibl  15078  rpcxpmul2  15500  fsumdvdsmul  15578  zabsle1  15591  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  lgsquad2lem2  15674  2lgs  15696  upgrpredgv  15850  upgredgpr  15853  bj-nnbist  15880  sumdc2  15935