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  442  pm2.24  610  con3rr3  622  expt  646  mtt  674  jaod  706  orel1  714  pm2.62  737  pm2.64  790  pm2.75  798  pm2.61ddc  846  peircedc  899  dcbi  920  pm5.62dc  929  pm4.83dc  935  ccased  949  3impd  1199  3expd  1202  mp3an1i  1308  pclem6  1352  simplbi2com  1420  19.21ht  1560  19.33b2  1608  equtrr  1686  spimeh  1717  cbv1  1722  equvini  1731  sbequ2  1742  ax11e  1768  ax11b  1798  sb6rf  1825  sb56  1857  exmoeudc  2060  moimv  2063  eupickbi  2079  exists2  2094  r19.12  2536  2gencl  2714  3gencl  2715  rspccv  2781  ceqex  2807  mo2icl  2858  mob  2861  euind  2866  reuind  2884  sseq2  3116  nelss  3153  difin  3308  reupick2  3357  uneqdifeqim  3443  difsn  3652  sssnm  3676  preq12b  3692  iinss2  3860  trintssm  4037  sspwb  4133  copsexg  4161  pocl  4220  pofun  4229  sowlin  4237  reusv1  4374  alxfr  4377  ralxfrALT  4383  iunpw  4396  onsucelsucr  4419  reg2exmidlema  4444  en2lp  4464  2optocl  4611  3optocl  4612  ssrel  4622  ssrel2  4624  ssrelrel  4634  relop  4684  xpidtr  4924  trin2  4925  poltletr  4934  xp11m  4972  relcnvtr  5053  iotaval  5094  funmo  5133  fss  5279  f0dom0  5311  fv3  5437  tz6.12c  5444  mpteqb  5504  funfvima  5642  f1veqaeq  5663  isoselem  5714  oprabid  5796  ovg  5902  fornex  6006  f1o2ndf1  6118  poxp  6122  tposfn2  6156  smoel  6190  tfri3  6257  nnaass  6374  nnmordi  6405  iinerm  6494  2ecoptocl  6510  3ecoptocl  6511  th3qlem2  6525  enm  6707  xpdom2  6718  xpf1o  6731  findcard2  6776  findcard2s  6777  eldju2ndl  6950  updjud  6960  distrnq0  7260  addassnq0  7263  prcdnql  7285  prcunqu  7286  nn0ge2m1nn  9030  nn0le2is012  9126  fzind  9159  nn0ind-raph  9161  zindd  9162  uzin  9351  indstr  9381  xnn0xadd0  9643  icoshft  9766  fzen  9816  uzsubsubfz  9820  elfz1b  9863  elfz0ubfz0  9895  elfz0fzfz0  9896  fz0fzelfz0  9897  elfzmlbp  9902  elfzodifsumelfzo  9971  ssfzo12bi  9995  elfzonelfzo  10000  modfzo0difsn  10161  frec2uzuzd  10168  expcllem  10297  mulexp  10325  leexp2r  10340  bernneq  10405  facdiv  10477  cjexp  10658  absexp  10844  clim2prod  11301  prodfap0  11307  prodfrecap  11308  addmodlteqALT  11546  oddge22np1  11567  nn0enne  11588  nn0o1gt2  11591  gcdneg  11659  dfgcd2  11691  rplpwr  11704  coprmdvds1  11761  qredeq  11766  cncongr1  11773  cncongr2  11774  prm2orodd  11796  setsn0fun  11985  fiinopn  12160  tgcl  12222  distop  12243  ssnei2  12315  tgcnp  12367  cnpnei  12377  cnmptcom  12456  neibl  12649  bj-nnbist  12942  sumdc2  12995