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

Theorem 3com23 1121
 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 1114 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 76 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1109 1 ((𝜑𝜒𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114  df-3an 898 This theorem is referenced by:  3coml  1122  syld3an2  1193  3anidm13  1204  eqreu  2756  f1ofveu  5528  acexmid  5539  dfsmo2  5933  f1oeng  6268  ltexprlemdisj  6762  ltexprlemfu  6767  recexprlemss1u  6792  mul32  7204  add32  7233  cnegexlem2  7250  subsub23  7279  subadd23  7286  addsub12  7287  subsub  7304  subsub3  7306  sub32  7308  suble  7509  lesub  7510  ltsub23  7511  ltsub13  7512  ltleadd  7515  div32ap  7745  div13ap  7746  div12ap  7747  divdiv32ap  7771  cju  7989  icc0r  8896  fzen  9009  elfz1b  9054  elfzmlbmOLD  9091  ioo0  9216  ico0  9218  ioc0  9219  expival  9422  expgt0  9453  expge0  9456  expge1  9457  shftval2  9655  abs3dif  9932  divalgb  10237
 Copyright terms: Public domain W3C validator