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

Theorem ancom2s 536
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 282 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
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 is referenced by:  an42s  559  ordsuc  4416  xpexr2m  4916  f1elima  5606  f1imaeq  5608  isosolem  5657  caovlem2d  5895  2ndconst  6049  isotilem  6808  prarloclem4  7207  mulsub  8030  leltadd  8076  eqord1  8112  divmul24ap  8337  blcomps  12324  blcom  12325
  Copyright terms: Public domain W3C validator