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

Theorem 3com23 1204
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 1197 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1188 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 973
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 975
This theorem is referenced by:  3coml  1205  syld3an2  1280  3anidm13  1291  eqreu  2922  f1ofveu  5841  acexmid  5852  dfsmo2  6266  f1oeng  6735  ctssdc  7090  ltexprlemdisj  7568  ltexprlemfu  7573  recexprlemss1u  7598  mul32  8049  add32  8078  cnegexlem2  8095  subsub23  8124  subadd23  8131  addsub12  8132  subsub  8149  subsub3  8151  sub32  8153  suble  8359  lesub  8360  ltsub23  8361  ltsub13  8362  ltleadd  8365  div32ap  8609  div13ap  8610  div12ap  8611  divdiv32ap  8637  cju  8877  icc0r  9883  fzen  9999  elfz1b  10046  ioo0  10216  ico0  10218  ioc0  10219  expgt0  10509  expge0  10512  expge1  10513  shftval2  10790  abs3dif  11069  divalgb  11884  nnwodc  11991  ctinf  12385  grpinvcnv  12767  restin  12970  cnpnei  13013  cnptoprest  13033  psmetsym  13123  xmetsym  13162
  Copyright terms: Public domain W3C validator