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

Theorem 3com23 1191
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com23 ((𝜑𝜒𝜓) → 𝜃)

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213exp 1184 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1176 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 963
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 965
This theorem is referenced by:  3coml  1192  syld3an2  1267  3anidm13  1278  eqreu  2904  f1ofveu  5812  acexmid  5823  dfsmo2  6234  f1oeng  6702  ctssdc  7057  ltexprlemdisj  7526  ltexprlemfu  7531  recexprlemss1u  7556  mul32  8005  add32  8034  cnegexlem2  8051  subsub23  8080  subadd23  8087  addsub12  8088  subsub  8105  subsub3  8107  sub32  8109  suble  8315  lesub  8316  ltsub23  8317  ltsub13  8318  ltleadd  8321  div32ap  8565  div13ap  8566  div12ap  8567  divdiv32ap  8593  cju  8832  icc0r  9830  fzen  9945  elfz1b  9992  ioo0  10159  ico0  10161  ioc0  10162  expgt0  10452  expge0  10455  expge1  10456  shftval2  10726  abs3dif  11005  divalgb  11816  ctinf  12170  restin  12587  cnpnei  12630  cnptoprest  12650  psmetsym  12740  xmetsym  12779
  Copyright terms: Public domain W3C validator