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

Theorem sylbird 169
 Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1 (𝜑 → (𝜒𝜓))
sylbird.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
sylbird (𝜑 → (𝜓𝜃))

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3 (𝜑 → (𝜒𝜓))
21biimprd 157 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 45 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 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:  3imtr3d  201  drex1  1770  eqreu  2876  onsucsssucr  4425  ordsucunielexmid  4446  ovi3  5907  tfrlem9  6216  dom2lem  6666  distrlem4prl  7399  distrlem4pru  7400  recexprlemm  7439  caucvgprlem1  7494  caucvgprprlemexb  7522  aptisr  7594  map2psrprg  7620  renegcl  8030  addid0  8142  remulext2  8369  mulext1  8381  apmul1  8555  nnge1  8750  0mnnnnn0  9016  nn0lt2  9139  zneo  9159  uzind2  9170  fzind  9173  nn0ind-raph  9175  ledivge1le  9520  elfzmlbp  9916  difelfznle  9919  elfzodifsumelfzo  9985  ssfzo12  10008  flqeqceilz  10098  addmodlteq  10178  uzsinds  10222  facdiv  10491  facwordi  10493  bcpasc  10519  addcn2  11086  mulcn2  11088  climrecvg1n  11124  odd2np1  11577  oddge22np1  11585  gcdaddm  11679  algcvgblem  11737  cncongr1  11791  metss2lem  12676
 Copyright terms: Public domain W3C validator