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  4476  rexxfrd  4477  poirr2  5035  smoel  6318  genprndl  7537  genprndu  7538  addcanprlemu  7631  leltadd  8421  lemul12b  8835  lbzbi  9633  dvdssub2  11859  odzdvds  12262
  Copyright terms: Public domain W3C validator