Theorem 3com23 839

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 832	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com23 32	. 2 |- (ph -> (ch -> (ps -> th)))
4	3	3imp 827	1 |- ((ph /\ ch /\ ps) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3coml 840  syld3an2 872  3anidm13 883  tfinds 3161  f1ofveu 3882  nneob 4255  add23t 5337  cnegextlem2 5346  subsub23t 5376  subadd23t 5385  addsub12t 5386  mul23t 5419  subsubt 5462  subsub3t 5463  sub23t 5465  sublet 5635  lesubt 5636  ltsub23t 5641  ltsub13t 5642  ltleaddt 5645  div13t 5743  qbtwnre 6278  shftval2t 6347  iooval2t 6367  ioo0t 6368  elioo4g 6385  expcant 6601  expordt 6602  exple1t 6607  abs3dift 6899  climsqueeze2 7141  caucvglem6 7162  fsum0diag4 7261  acdc2lem1 7488  acdc5lem1 7491  infxpabs 7570  infxpdom 7571  infmap2 7581  metsym 7816  metcnpi3 7892  lmnn 7935  lmuni 7951  lmle 7960  grpidinvlem2 8049  grpinvdiv 8084  nvpncan 8277  nvsub 8295  nvabs 8301  nvelbl 8325  ipval2lem2 8354  ipval2lem5 8360  ipcj 8367  iporthcom 8369  ipdi 8503  ipassr 8506  ipsubdi 8509  hlipcj 8613  hvadd23t 8903  his5t 8953  hoadd23t 9709  hosubsubt 9743  unopf1ot 9840  adj2t 9858  adjvalvalt 9861  brafnmult 9875  adjlnopt 10019  leopmul2it 10068  cvntrt 10219  mdsymlem5 10334  sumdmdi 10342  ghomf1olem 10396  elioo1t3 10496  idfisf 10760

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 777

Copyright terms: Public domain