Theorem 3coml 839

Description: Commutation in antecedent. Rotate left.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3coml	|- ((ps /\ ch /\ ph) -> th)

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3com23 838	. 2 |- ((ph /\ ch /\ ps) -> th)
3	2	3com13 837	1 |- ((ps /\ ch /\ ph) -> th)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  3comr 840  funbrfvbg 3748  oaword 4173  omwordri 4193  ltapq 5056  ltmpq 5057  ltasr 5189  adddirt 5299  addcan2t 5333  subdirt 5408  nnncan1t 5447  pnpcan2t 5459  axltadd 5485  ltaddsubt 5613  leaddsubt 5615  lesub2t 5642  ltsub2t 5644  mulcan2t 5670  div13t 5714  divcan5t 5745  ltdiv2t 5843  lediv2t 5847  lble 6002  qbtwnre 6224  iooint 6317  iooss2 6319  fzrevral2t 6460  fzshftralt 6462  faclbnd5 6898  isummulc1ALT 7156  rescncf 7215  mettri 7767  metxp 7786  cnmet 7856  bl2ioo 7863  ghgrpi 8089  vcdir 8124  vcass 8125  imsmetlem 8274  hvaddcan2t 8877  hvsubcan2t 8881  pjeq2t 9179

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776

Copyright terms: Public domain