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

Theorem 3com23 1187
 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 1180 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1175 1 ((𝜑𝜒𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962 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 964 This theorem is referenced by:  3coml  1188  syld3an2  1263  3anidm13  1274  eqreu  2876  f1ofveu  5762  acexmid  5773  dfsmo2  6184  f1oeng  6651  ctssdc  6998  ltexprlemdisj  7414  ltexprlemfu  7419  recexprlemss1u  7444  mul32  7892  add32  7921  cnegexlem2  7938  subsub23  7967  subadd23  7974  addsub12  7975  subsub  7992  subsub3  7994  sub32  7996  suble  8202  lesub  8203  ltsub23  8204  ltsub13  8205  ltleadd  8208  div32ap  8452  div13ap  8453  div12ap  8454  divdiv32ap  8480  cju  8719  icc0r  9709  fzen  9823  elfz1b  9870  ioo0  10037  ico0  10039  ioc0  10040  expgt0  10326  expge0  10329  expge1  10330  shftval2  10598  abs3dif  10877  divalgb  11622  ctinf  11943  restin  12345  cnpnei  12388  cnptoprest  12408  psmetsym  12498  xmetsym  12537
 Copyright terms: Public domain W3C validator