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

Theorem an32s 563
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 557 . 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  566  anabss1  571  fssres  5373  foco  5430  fun11iun  5463  fconstfvm  5714  isocnv  5790  f1oiso  5805  f1ocnvfv3  5842  tfrcl  6343  mapxpen  6826  findcard  6866  exmidfodomrlemim  7178  genpassl  7486  genpassu  7487  axsuploc  7992  cnegexlem3  8096  recexaplem2  8570  divap0  8601  dfinfre  8872  qreccl  9601  xrlttr  9752  addmodlteq  10354  cau3lem  11078  climcn1  11271  climcn2  11272  climcaucn  11314  ntrivcvgap  11511  rplpwr  11982  dvdssq  11986  nn0seqcvgd  11995  lcmgcdlem  12031  isprm6  12101  phiprmpw  12176  pcneg  12278  prmpwdvds  12307  grpinveu  12741  tgcl  12858  innei  12957  cncnp  13024  cnnei  13026  elbl2ps  13186  elbl2  13187  cncfco  13372  cnlimc  13435
  Copyright terms: Public domain W3C validator