ILE Home 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  5053  foco  5103  fun11iun  5134  fconstfvm  5366  isocnv  5438  f1oiso  5452  f1ocnvfv3  5488  findcard  6331  genpassl  6603  genpassu  6604  cnegexlem3  7168  recexaplem2  7609  divap0  7639  qreccl  8547  xrlttr  8683  cau3lem  9588  climcn1  9706  climcn2  9707  climcaucn  9747  nn0seqcvgd  9757
  Copyright terms: Public domain W3C validator