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

Theorem an32s 502
 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 496 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 114 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  anass1rs  505  anabss1  510  fssres  5066  foco  5116  fun11iun  5147  fconstfvm  5379  isocnv  5451  f1oiso  5465  f1ocnvfv3  5501  findcard  6345  genpassl  6622  genpassu  6623  cnegexlem3  7188  recexaplem2  7633  divap0  7663  qreccl  8576  xrlttr  8716  cau3lem  9710  climcn1  9829  climcn2  9830  climcaucn  9870  nn0seqcvgd  9880
 Copyright terms: Public domain W3C validator