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

Theorem an32s 540
 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 534 . 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  543  anabss1  548  fssres  5266  foco  5323  fun11iun  5354  fconstfvm  5604  isocnv  5678  f1oiso  5693  f1ocnvfv3  5729  tfrcl  6227  mapxpen  6708  findcard  6748  exmidfodomrlemim  7021  genpassl  7296  genpassu  7297  axsuploc  7801  cnegexlem3  7903  recexaplem2  8373  divap0  8404  dfinfre  8671  qreccl  9383  xrlttr  9521  addmodlteq  10111  cau3lem  10826  climcn1  11017  climcn2  11018  climcaucn  11060  rplpwr  11611  dvdssq  11615  nn0seqcvgd  11618  lcmgcdlem  11654  isprm6  11721  phiprmpw  11793  tgcl  12128  innei  12227  cncnp  12294  cnnei  12296  elbl2ps  12456  elbl2  12457  cncfco  12642  cnlimc  12693
 Copyright terms: Public domain W3C validator