Theorem com3l 34

Description: Commutation of antecedents. Rotate left.

Hypothesis

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

Assertion

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

Proof of Theorem com3l

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

Syntax hints:   -> wi 2

This theorem is referenced by:  com3r 35  com4l 39  prlem1 576  prel12 1875  tfindsg 2402  fvco2 2866  isofrlem 2939  tfrlem9 2957  tfr3 2964  oawordri 3152  nndi 3180  nnmass 3181  rankr1 3518  aceq6b 3565  zornlem7 3609  imadomg 3616  unxpdomlem 3649  genpnmax 3904  ltexprlem1 3936  ssgt0sr 4011  axrecex 4079  nnleltp1t 4448  zneo 4601  expaddt 4698  infxpidmlem7 4939  shscl 5282  5oalem6 5549  atom1d 5750  mdsymlem4 5779

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org