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

Theorem ancom2s 555
 Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
an12s.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
ancom2s ((𝜑 ∧ (𝜒𝜓)) → 𝜃)

Proof of Theorem ancom2s
StepHypRef Expression
1 pm3.22 263 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 284 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 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 is referenced by:  an42s  578  ordsuc  4478  xpexr2m  4980  f1elima  5674  f1imaeq  5676  isosolem  5725  caovlem2d  5963  2ndconst  6119  isotilem  6893  prarloclem4  7318  mulsub  8175  leltadd  8221  eqord1  8257  divmul24ap  8488  blcomps  12579  blcom  12580
 Copyright terms: Public domain W3C validator