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  98  expcom  115  impcom  124  syl5ibcom  154  syl5ibrcom  156  pm5.501  243  impd  252  expd  256  pm3.21  262  imdistanri  443  pm2.24  611  con3rr3  623  expt  647  mtt  675  jaod  707  orel1  715  pm2.62  738  pm2.64  791  pm2.75  799  pm2.61ddc  851  peircedc  904  dcbi  926  pm5.62dc  935  pm4.83dc  941  ccased  955  3impd  1211  3expd  1214  mp3an1i  1320  pclem6  1364  simplbi2com  1432  19.21ht  1569  19.33b2  1617  equtrr  1698  spimeh  1727  cbv1  1733  cbv1v  1735  equvini  1746  sbequ2  1757  ax11e  1784  ax11b  1814  sb6rf  1841  sb56  1873  exmoeudc  2077  moimv  2080  eupickbi  2096  exists2  2111  r19.12  2571  2gencl  2758  3gencl  2759  rspccv  2826  ceqex  2852  mo2icl  2904  mob  2907  euind  2912  reuind  2930  sseq2  3165  nelss  3202  difin  3358  reupick2  3407  uneqdifeqim  3493  difsn  3709  sssnm  3733  preq12b  3749  iinss2  3917  trintssm  4095  sspwb  4193  copsexg  4221  pocl  4280  pofun  4289  sowlin  4297  reusv1  4435  alxfr  4438  ralxfrALT  4444  iunpw  4457  onsucelsucr  4484  reg2exmidlema  4510  en2lp  4530  2optocl  4680  3optocl  4681  ssrel  4691  ssrel2  4693  ssrelrel  4703  relop  4753  xpidtr  4993  trin2  4994  poltletr  5003  xp11m  5041  relcnvtr  5122  iotaval  5163  funmo  5202  fss  5348  f0dom0  5380  fv3  5508  tz6.12c  5515  mpteqb  5575  funfvima  5715  f1veqaeq  5736  isoselem  5787  oprabid  5870  ovg  5976  fornex  6080  f1o2ndf1  6192  poxp  6196  tposfn2  6230  smoel  6264  tfri3  6331  nnaass  6449  nnmordi  6480  iinerm  6569  2ecoptocl  6585  3ecoptocl  6586  th3qlem2  6600  enm  6782  xpdom2  6793  xpf1o  6806  findcard2  6851  findcard2s  6852  eldju2ndl  7033  updjud  7043  distrnq0  7396  addassnq0  7399  prcdnql  7421  prcunqu  7422  nn0ge2m1nn  9170  nn0le2is012  9269  fzind  9302  nn0ind-raph  9304  zindd  9305  uzin  9494  indstr  9527  xnn0xadd0  9799  icoshft  9922  fzen  9974  uzsubsubfz  9978  elfz1b  10021  elfz0ubfz0  10056  elfz0fzfz0  10057  fz0fzelfz0  10058  elfzmlbp  10063  elfzodifsumelfzo  10132  ssfzo12bi  10156  elfzonelfzo  10161  modfzo0difsn  10326  frec2uzuzd  10333  expcllem  10462  mulexp  10490  leexp2r  10505  bernneq  10571  facdiv  10647  cjexp  10831  absexp  11017  clim2prod  11476  prodfap0  11482  prodfrecap  11483  prodmodc  11515  fprodabs  11553  addmodlteqALT  11793  oddge22np1  11814  nn0enne  11835  nn0o1gt2  11838  gcdneg  11911  dfgcd2  11943  rplpwr  11956  coprmdvds1  12019  qredeq  12024  cncongr1  12031  cncongr2  12032  prm2orodd  12054  nnnn0modprm0  12183  prm23lt5  12191  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  oddprmdvds  12280  prmpwdvds  12281  setsn0fun  12427  fiinopn  12602  tgcl  12664  distop  12685  ssnei2  12757  tgcnp  12809  cnpnei  12819  cnmptcom  12898  neibl  13091  zabsle1  13500  bj-nnbist  13585  sumdc2  13640