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

Theorem ancomsd 269
Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
Hypothesis
Ref Expression
ancomsd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
ancomsd (𝜑 → ((𝜒𝜓) → 𝜃))

Proof of Theorem ancomsd
StepHypRef Expression
1 ancom 266 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
2 ancomsd.1 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
31, 2biimtrid 152 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  sylan2d  294  mpand  429  anabsi6  580  ralxfrd  4463  rexxfrd  4464  poirr2  5022  smoel  6301  genprndl  7520  genprndu  7521  addcanprlemu  7614  leltadd  8404  lemul12b  8818  lbzbi  9616  dvdssub2  11842  odzdvds  12245
  Copyright terms: Public domain W3C validator