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

Theorem an32s 558
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 552 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 120 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 depends on definitions:  df-bi 116
This theorem is referenced by:  anass1rs  561  anabss1  566  fssres  5345  foco  5402  fun11iun  5435  fconstfvm  5685  isocnv  5761  f1oiso  5776  f1ocnvfv3  5813  tfrcl  6311  mapxpen  6793  findcard  6833  exmidfodomrlemim  7136  genpassl  7444  genpassu  7445  axsuploc  7950  cnegexlem3  8052  recexaplem2  8526  divap0  8557  dfinfre  8827  qreccl  9551  xrlttr  9702  addmodlteq  10297  cau3lem  11014  climcn1  11205  climcn2  11206  climcaucn  11248  ntrivcvgap  11445  rplpwr  11911  dvdssq  11915  nn0seqcvgd  11918  lcmgcdlem  11954  isprm6  12022  phiprmpw  12097  tgcl  12475  innei  12574  cncnp  12641  cnnei  12643  elbl2ps  12803  elbl2  12804  cncfco  12989  cnlimc  13052
  Copyright terms: Public domain W3C validator