Theorem com3r 35

Description: Commutation of antecedents. Rotate right.

Hypothesis

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

Assertion

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

Proof of Theorem com3r

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- (ph -> (ps -> (ch -> th)))
2	1	com3l 34	. 2 |- (ps -> (ch -> (ph -> th)))
3	2	com3l 34	1 |- (ch -> (ph -> (ps -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  moexex 1478  vtocl3ga 1900  onfr 3014  ordsssuc2 3060  limuni3 3206  fvco 3885  fvco2 3886  eqfnfv 3909  eqfnfv2 3911  tfrlem5 4216  tz7.49 4260  omcl 4307  oecl 4308  omwordri 4339  odi 4346  omass 4347  oewordri 4355  nnmcl 4370  nnecl 4371  oaabs 4392  f1oen2g 4535  f1domg 4537  ac6sfi 4591  tz9.12lem3 4807  zorn2lem5 4938  zorn2lem6 4939  unidom 4954  cardlim 5001  alephordi 5024  alephval2 5052  alephval3 5053  psslinpr 5289  ltaprlem 5304  prlem936b 5308  suppsr3 5378  lbreu 6213  zneo 6371  uzwo5OLD 6382  climserzlei 7350  caucvgi 7366  cvgratlem2 7456  infxpidmlem12 7775  cnsscnp 7982  hausnei 7994  mettri4 8024  opnin 8079  spwmo 8918  efifolem4 8997  hlim0 9381  chintcli 9571  spansni 9756  h1datomi 9780  strlem3a 10460  hstrlem3a 10468  mdexchi 10543  cvbr3i 10575  mdsymlem4 10615  mdsymlem6 10617  uninqs 10730  11st22nd 10742  ref3w 10772  set2elt 10827  pospos 10882  cnvhmphb 11032  top2ind 11050  oefil2 11079  cnfilca 11088  bwt2 11123  cmpassoh 11256  cmpmon 11270  efp2 11321  ioodisj 11413  ordtypelem7 11433  opncldf1 11454  hausnei2 11471  compsublem 11487  compsub 11488  dfcon2 11501  fbssint 11626  fbunfip 11631  cnpfillim 11686  morex 11804  fimax 11837

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

Copyright terms: Public domain