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

Theorem sylbird 163
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 151 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr3d  195  drex1  1695  eqreu  2755  onsucsssucr  4262  ordsucunielexmid  4283  ovi3  5664  tfrlem9  5965  rdgon  6003  dom2lem  6282  distrlem4prl  6739  distrlem4pru  6740  recexprlemm  6779  caucvgprlem1  6834  caucvgprprlemexb  6862  aptisr  6920  renegcl  7334  addid0  7442  remulext2  7664  mulext1  7676  apmul1  7838  nnge1  8012  0mnnnnn0  8270  nn0lt2  8379  zneo  8397  uzind2  8408  fzind  8411  nn0ind-raph  8413  ledivge1le  8749  elfzmlbp  9091  difelfznle  9094  elfzodifsumelfzo  9158  ssfzo12  9181  flqeqceilz  9267  addmodlteq  9347  facdiv  9605  facwordi  9607  bcpasc  9633  addcn2  10061  mulcn2  10063  climrecvg1n  10097  odd2np1  10183  oddge22np1  10192  algcvgblem  10250
  Copyright terms: Public domain W3C validator