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

Theorem 3com23 1147
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 1140 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 77 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1135 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 922
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 924
This theorem is referenced by:  3coml  1148  syld3an2  1219  3anidm13  1230  eqreu  2798  f1ofveu  5601  acexmid  5612  dfsmo2  6006  f1oeng  6426  ltexprlemdisj  7109  ltexprlemfu  7114  recexprlemss1u  7139  mul32  7556  add32  7585  cnegexlem2  7602  subsub23  7631  subadd23  7638  addsub12  7639  subsub  7656  subsub3  7658  sub32  7660  suble  7862  lesub  7863  ltsub23  7864  ltsub13  7865  ltleadd  7868  div32ap  8098  div13ap  8099  div12ap  8100  divdiv32ap  8126  cju  8356  icc0r  9276  fzen  9389  elfz1b  9434  ioo0  9599  ico0  9601  ioc0  9602  expival  9856  expgt0  9887  expge0  9890  expge1  9891  shftval2  10157  abs3dif  10434  divalgb  10807
  Copyright terms: Public domain W3C validator