Theorem 3coml 852

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 851	. 2 |- ((ph /\ ch /\ ps) -> th)
3	2	3com13 850	1 |- ((ps /\ ch /\ ph) -> th)

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  3comr 853  funbrfvbg 3814  oaword 4241  omwordri 4261  ltapq 5141  ltmpq 5142  ltasr 5274  adddir 5384  addcan2 5418  subdir 5493  nnncan1 5532  pnpcan2 5544  axltadd 5570  ltaddsub 5696  leaddsub 5698  lesub2 5726  ltsub2 5728  mulcan2OLD 5758  div13 5806  divcan5 5839  ltdiv2 5947  lediv2 5951  nndiv 6020  lble 6129  zdiv 6270  qbtwnre 6331  iooin 6397  iooss2 6399  fzrevral2 6546  fzshftral 6548  faclbnd5 7043  isummulc1iALT 7303  rescncf 7362  mettri 7902  metxp 7919  cnmet 7989  bl2ioo 7996  ghgrpi 8221  vcdir 8256  vcass 8257  imsmetlem 8407  hvaddcan2 9021  hvsubcan2 9025  pjeq2 9324

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 154  df-an 232  df-3an 789

Copyright terms: Public domain