Theorem 3com23 841

Description: Commutation in antecedent. Swap 2nd and 3rd.

Hypothesis

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

Assertion

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

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 834	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com23 32	. 2 |- (ph -> (ch -> (ps -> th)))
4	3	3imp 829	1 |- ((ph /\ ch /\ ps) -> th)

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  3coml 842  syld3an2 874  3anidm13 885  tfinds 3167  f1ofveu 3888  nneob 4261  add23t 5349  cnegextlem2 5358  subsub23t 5388  subadd23t 5397  addsub12t 5398  mul23t 5431  subsubt 5474  subsub3t 5475  sub23t 5477  sublet 5647  lesubt 5648  ltsub23t 5653  ltsub13t 5654  ltleaddt 5657  div13t 5750  qbtwnre 6279  shftval2t 6348  iooval2t 6368  ioo0t 6369  elioo4g 6386  expcant 6602  expordt 6603  exple1t 6608  abs3dift 6899  climsqueeze2 7141  caucvglem6 7162  fsum0diag4 7261  acdc2lem1 7489  acdc5lem1 7492  infxpabs 7571  infxpdom 7572  infmap2 7583  metsym 7813  metcnpi3 7889  lmnn 7932  lmuni 7948  lmle 7957  grpidinvlem2 8046  grpinvdiv 8080  nvpncan 8273  nvsub 8291  nvabs 8297  nvelbl 8321  ipval2lem2 8350  ipval2lem5 8356  ipcj 8363  iporthcom 8365  ipdi 8499  ipassr 8502  ipsubdi 8505  hlipcj 8609  hvadd23t 8898  his5t 8948  hoadd23t 9704  hosubsubt 9738  unopf1ot 9835  adj2t 9853  adjvalvalt 9856  brafnmult 9870  adjlnopt 10014  leopmul2it 10063  cvntrt 10214  mdsymlem5 10329  sumdmdi 10337  ghomf1olem 10391  elioo1t3 10482  idfisf 10731

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 779

Copyright terms: Public domain