Theorem com13 33

Description: Commutation of antecedents. Swap 1st and 3rd.

Hypothesis

Ref	Expression
com3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
com13	|- (ch -> (ps -> (ph -> th)))

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . . 4 |- (ph -> (ps -> (ch -> th)))
2	1	com12 11	. . 3 |- (ps -> (ph -> (ch -> th)))
3	2	com23 32	. 2 |- (ps -> (ch -> (ph -> th)))
4	3	com12 11	1 |- (ch -> (ps -> (ph -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  com3l 34  com14 38  ancom13s 491  ancom31s 494  dn1 779  ordsssuc2 3060  peano5 3241  funopg 3652  isomin 4013  abianfp 4263  omordi 4333  brecop 4447  ac6sfilem3 4590  isfinite2 4692  fiint 4703  aceq5 4886  aceq6b 4888  carduni 5008  mulgt0sr 5368  squeeze0 6069  xrsupsslem 6244  xrinfmsslem 6245  supxrunb1 6257  supxrunb2 6258  zmax 6392  facwordi 7147  infxpidmlem7 7770  infxpidmlem12 7775  cnpco 7979  iscncl 7980  cncnplem4 7987  opnin 8079  metequiv 8091  lmle 8171  bcthlem1 8210  bcthlem28 8237  bcthlem33 8242  vacnlem3 8584  spwmo 8918  projlem15 9476  projlem26 9487  shmodsi 9638  kbass6 10334  mdsymlem6 10617  mdsymlem7 10618  cdj3lem2a 10645  cdj3lem3a 10648  uninqs 10730  fiiu 10738  11st22nd 10742  f1fi 10779  prj1 10809  set2elt 10827  lteqtpos 10880  grpmnd 10933  rnplrnml3 10950  ununr 10955  on1el3 10962  on1el4 10963  uznzr 10967  cdrci 10994  top2usne 11051  homindlem3 11053  fipfil2 11077  efilcp 11083  filint2 11084  efilcp2 11087  cnfilca 11088  rcfpfillem2 11090  rcfpfillem6 11094  bwt2 11123  usinuniop 11128  topsinind 11136  iintlem1 11155  cmpassoh 11256  ismonc 11269  cmpmon 11270  icmpmon 11271  isepic 11279  idsubfun 11312  ordtypelem5 11431  omsubindss 11449  opncldf1 11454  compfipin0 11493  cncomp 11494  reconn 11512  topmtcl 11586  fnejoin1 11591  fnejoin2 11592  flimopn 11679  limfilcf 11683  hausfillim 11685  fclsfnflim 11726  fcluscomplem 11732  gaass 11781  gapmlem 11783  gapm 11784  findcard 11836  fimax 11837  inficl 11849  lmtlm 11969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain