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  4462  rexxfrd  4463  poirr2  5021  smoel  6300  genprndl  7519  genprndu  7520  addcanprlemu  7613  leltadd  8403  lemul12b  8817  lbzbi  9615  dvdssub2  11841  odzdvds  12244
  Copyright terms: Public domain W3C validator