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

Theorem 3com23 1170
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 1163 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 78 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1158 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3coml  1171  syld3an2  1246  3anidm13  1257  eqreu  2847  f1ofveu  5728  acexmid  5739  dfsmo2  6150  f1oeng  6617  ctssdc  6964  ltexprlemdisj  7378  ltexprlemfu  7383  recexprlemss1u  7408  mul32  7856  add32  7885  cnegexlem2  7902  subsub23  7931  subadd23  7938  addsub12  7939  subsub  7956  subsub3  7958  sub32  7960  suble  8166  lesub  8167  ltsub23  8168  ltsub13  8169  ltleadd  8172  div32ap  8412  div13ap  8413  div12ap  8414  divdiv32ap  8440  cju  8676  icc0r  9649  fzen  9763  elfz1b  9810  ioo0  9977  ico0  9979  ioc0  9980  expgt0  10266  expge0  10269  expge1  10270  shftval2  10538  abs3dif  10817  divalgb  11518  ctinf  11838  restin  12240  cnpnei  12283  cnptoprest  12303  psmetsym  12393  xmetsym  12432
  Copyright terms: Public domain W3C validator