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

Theorem 3com23 1152
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 1145 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1140 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  3coml  1153  syld3an2  1228  3anidm13  1239  eqreu  2821  f1ofveu  5678  acexmid  5689  dfsmo2  6090  f1oeng  6554  ltexprlemdisj  7262  ltexprlemfu  7267  recexprlemss1u  7292  mul32  7709  add32  7738  cnegexlem2  7755  subsub23  7784  subadd23  7791  addsub12  7792  subsub  7809  subsub3  7811  sub32  7813  suble  8015  lesub  8016  ltsub23  8017  ltsub13  8018  ltleadd  8021  div32ap  8256  div13ap  8257  div12ap  8258  divdiv32ap  8284  cju  8519  icc0r  9492  fzen  9606  elfz1b  9653  ioo0  9820  ico0  9822  ioc0  9823  expgt0  10103  expge0  10106  expge1  10107  shftval2  10375  abs3dif  10653  divalgb  11352  restin  12028  cnpnei  12070  cnptoprest  12090  psmetsym  12115  xmetsym  12154
  Copyright terms: Public domain W3C validator