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

Theorem 3com23 1211
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 1204 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 78 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1195 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1307  eqreu  2953  f1ofveu  5907  acexmid  5918  dfsmo2  6342  f1oeng  6813  ctssdc  7174  ltexprlemdisj  7668  ltexprlemfu  7673  recexprlemss1u  7698  mul32  8151  add32  8180  cnegexlem2  8197  subsub23  8226  subadd23  8233  addsub12  8234  subsub  8251  subsub3  8253  sub32  8255  suble  8461  lesub  8462  ltsub23  8463  ltsub13  8464  ltleadd  8467  div32ap  8713  div13ap  8714  div12ap  8715  divdiv32ap  8741  cju  8982  icc0r  9995  fzen  10112  elfz1b  10159  ioo0  10331  ico0  10333  ioc0  10334  expgt0  10646  expge0  10649  expge1  10650  shftval2  10973  abs3dif  11252  divalgb  12069  nnwodc  12176  ctinf  12590  grpinvcnv  13143  mulgaddcom  13219  mulgneg2  13229  srgrmhm  13493  ringcom  13530  mulgass2  13557  opprrng  13576  opprring  13578  unitmulcl  13612  islmodd  13792  lmodcom  13832  rmodislmod  13850  restin  14355  cnpnei  14398  cnptoprest  14418  psmetsym  14508  xmetsym  14547
  Copyright terms: Public domain W3C validator