ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3com23 Unicode version

Theorem 3com23 1145
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3com23  |-  ( (
ph  /\  ch  /\  ps )  ->  th )

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1138 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 77 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1133 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3coml  1146  syld3an2  1217  3anidm13  1228  eqreu  2785  f1ofveu  5531  acexmid  5542  dfsmo2  5936  f1oeng  6304  ltexprlemdisj  6858  ltexprlemfu  6863  recexprlemss1u  6888  mul32  7305  add32  7334  cnegexlem2  7351  subsub23  7380  subadd23  7387  addsub12  7388  subsub  7405  subsub3  7407  sub32  7409  suble  7611  lesub  7612  ltsub23  7613  ltsub13  7614  ltleadd  7617  div32ap  7847  div13ap  7848  div12ap  7849  divdiv32ap  7875  cju  8105  icc0r  9025  fzen  9138  elfz1b  9183  ioo0  9346  ico0  9348  ioc0  9349  expival  9575  expgt0  9606  expge0  9609  expge1  9610  shftval2  9852  abs3dif  10129  divalgb  10469
  Copyright terms: Public domain W3C validator