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  444  pm2.24  616  con3rr3  628  expt  652  mtt  680  jaod  712  orel1  720  pm2.62  743  pm2.64  796  pm2.75  804  pm2.61ddc  856  peircedc  909  dcbi  931  pm5.62dc  940  pm4.83dc  946  ccased  960  3impd  1216  3expd  1219  mp3an1i  1325  pclem6  1369  simplbi2com  1437  19.21ht  1574  19.33b2  1622  equtrr  1703  spimeh  1732  cbv1  1738  cbv1v  1740  equvini  1751  sbequ2  1762  ax11e  1789  ax11b  1819  sb6rf  1846  sb56  1878  exmoeudc  2082  moimv  2085  eupickbi  2101  exists2  2116  r19.12  2576  2gencl  2763  3gencl  2764  rspccv  2831  ceqex  2857  mo2icl  2909  mob  2912  euind  2917  reuind  2935  sseq2  3171  nelss  3208  difin  3364  reupick2  3413  uneqdifeqim  3500  difsn  3717  sssnm  3741  preq12b  3757  iinss2  3925  trintssm  4103  sspwb  4201  copsexg  4229  pocl  4288  pofun  4297  sowlin  4305  reusv1  4443  alxfr  4446  ralxfrALT  4452  iunpw  4465  onsucelsucr  4492  reg2exmidlema  4518  en2lp  4538  2optocl  4688  3optocl  4689  ssrel  4699  ssrel2  4701  ssrelrel  4711  relop  4761  xpidtr  5001  trin2  5002  poltletr  5011  xp11m  5049  relcnvtr  5130  iotaval  5171  funmo  5213  fss  5359  f0dom0  5391  fv3  5519  tz6.12c  5526  mpteqb  5586  funfvima  5727  f1veqaeq  5748  isoselem  5799  oprabid  5885  ovg  5991  fornex  6094  f1o2ndf1  6207  poxp  6211  tposfn2  6245  smoel  6279  tfri3  6346  nnaass  6464  nnmordi  6495  iinerm  6585  2ecoptocl  6601  3ecoptocl  6602  th3qlem2  6616  enm  6798  xpdom2  6809  xpf1o  6822  findcard2  6867  findcard2s  6868  eldju2ndl  7049  updjud  7059  distrnq0  7421  addassnq0  7424  prcdnql  7446  prcunqu  7447  nn0ge2m1nn  9195  nn0le2is012  9294  fzind  9327  nn0ind-raph  9329  zindd  9330  uzin  9519  indstr  9552  xnn0xadd0  9824  icoshft  9947  fzen  9999  uzsubsubfz  10003  elfz1b  10046  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  elfzmlbp  10088  elfzodifsumelfzo  10157  ssfzo12bi  10181  elfzonelfzo  10186  modfzo0difsn  10351  frec2uzuzd  10358  expcllem  10487  mulexp  10515  leexp2r  10530  bernneq  10596  facdiv  10672  cjexp  10857  absexp  11043  clim2prod  11502  prodfap0  11508  prodfrecap  11509  prodmodc  11541  fprodabs  11579  addmodlteqALT  11819  oddge22np1  11840  nn0enne  11861  nn0o1gt2  11864  gcdneg  11937  dfgcd2  11969  rplpwr  11982  coprmdvds1  12045  qredeq  12050  cncongr1  12057  cncongr2  12058  prm2orodd  12080  nnnn0modprm0  12209  prm23lt5  12217  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  oddprmdvds  12306  prmpwdvds  12307  setsn0fun  12453  isnmgm  12614  sgrpass  12649  insubm  12703  fiinopn  12796  tgcl  12858  distop  12879  ssnei2  12951  tgcnp  13003  cnpnei  13013  cnmptcom  13092  neibl  13285  zabsle1  13694  bj-nnbist  13779  sumdc2  13834