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

Theorem an32s 510
 Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
an32s (((𝜑𝜒) ∧ 𝜓) → 𝜃)

Proof of Theorem an32s
StepHypRef Expression
1 an32 504 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 118 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  anass1rs  513  anabss1  518  fssres  5093  foco  5143  fun11iun  5174  fconstfvm  5406  isocnv  5478  f1oiso  5492  f1ocnvfv3  5528  findcard  6375  genpassl  6679  genpassu  6680  cnegexlem3  7250  recexaplem2  7706  divap0  7736  qreccl  8673  xrlttr  8816  addmodlteq  9347  cau3lem  9940  climcn1  10059  climcn2  10060  climcaucn  10100  nn0seqcvgd  10249
 Copyright terms: Public domain W3C validator