ILE Home 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