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  3499  difsn  3715  sssnm  3739  preq12b  3755  iinss2  3923  trintssm  4101  sspwb  4199  copsexg  4227  pocl  4286  pofun  4295  sowlin  4303  reusv1  4441  alxfr  4444  ralxfrALT  4450  iunpw  4463  onsucelsucr  4490  reg2exmidlema  4516  en2lp  4536  2optocl  4686  3optocl  4687  ssrel  4697  ssrel2  4699  ssrelrel  4709  relop  4759  xpidtr  4999  trin2  5000  poltletr  5009  xp11m  5047  relcnvtr  5128  iotaval  5169  funmo  5211  fss  5357  f0dom0  5389  fv3  5517  tz6.12c  5524  mpteqb  5584  funfvima  5725  f1veqaeq  5746  isoselem  5797  oprabid  5883  ovg  5989  fornex  6092  f1o2ndf1  6205  poxp  6209  tposfn2  6243  smoel  6277  tfri3  6344  nnaass  6462  nnmordi  6493  iinerm  6583  2ecoptocl  6599  3ecoptocl  6600  th3qlem2  6614  enm  6796  xpdom2  6807  xpf1o  6820  findcard2  6865  findcard2s  6866  eldju2ndl  7047  updjud  7057  distrnq0  7414  addassnq0  7417  prcdnql  7439  prcunqu  7440  nn0ge2m1nn  9188  nn0le2is012  9287  fzind  9320  nn0ind-raph  9322  zindd  9323  uzin  9512  indstr  9545  xnn0xadd0  9817  icoshft  9940  fzen  9992  uzsubsubfz  9996  elfz1b  10039  elfz0ubfz0  10074  elfz0fzfz0  10075  fz0fzelfz0  10076  elfzmlbp  10081  elfzodifsumelfzo  10150  ssfzo12bi  10174  elfzonelfzo  10179  modfzo0difsn  10344  frec2uzuzd  10351  expcllem  10480  mulexp  10508  leexp2r  10523  bernneq  10589  facdiv  10665  cjexp  10850  absexp  11036  clim2prod  11495  prodfap0  11501  prodfrecap  11502  prodmodc  11534  fprodabs  11572  addmodlteqALT  11812  oddge22np1  11833  nn0enne  11854  nn0o1gt2  11857  gcdneg  11930  dfgcd2  11962  rplpwr  11975  coprmdvds1  12038  qredeq  12043  cncongr1  12050  cncongr2  12051  prm2orodd  12073  nnnn0modprm0  12202  prm23lt5  12210  dvdsprmpweqnn  12282  dvdsprmpweqle  12283  oddprmdvds  12299  prmpwdvds  12300  setsn0fun  12446  isnmgm  12607  sgrpass  12642  insubm  12696  fiinopn  12761  tgcl  12823  distop  12844  ssnei2  12916  tgcnp  12968  cnpnei  12978  cnmptcom  13057  neibl  13250  zabsle1  13659  bj-nnbist  13744  sumdc2  13799