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

Theorem an32s 542
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 536 . 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  545  anabss1  550  fssres  5268  foco  5325  fun11iun  5356  fconstfvm  5606  isocnv  5680  f1oiso  5695  f1ocnvfv3  5731  tfrcl  6229  mapxpen  6710  findcard  6750  exmidfodomrlemim  7025  genpassl  7300  genpassu  7301  axsuploc  7805  cnegexlem3  7907  recexaplem2  8381  divap0  8412  dfinfre  8682  qreccl  9402  xrlttr  9549  addmodlteq  10139  cau3lem  10854  climcn1  11045  climcn2  11046  climcaucn  11088  rplpwr  11642  dvdssq  11646  nn0seqcvgd  11649  lcmgcdlem  11685  isprm6  11752  phiprmpw  11825  tgcl  12160  innei  12259  cncnp  12326  cnnei  12328  elbl2ps  12488  elbl2  12489  cncfco  12674  cnlimc  12737
  Copyright terms: Public domain W3C validator