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

Theorem sylbird 168
 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 156 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 44 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  3imtr3d  200  drex1  1721  eqreu  2794  onsucsssucr  4282  ordsucunielexmid  4303  ovi3  5690  tfrlem9  5990  dom2lem  6342  distrlem4prl  6913  distrlem4pru  6914  recexprlemm  6953  caucvgprlem1  7008  caucvgprprlemexb  7036  aptisr  7094  renegcl  7513  addid0  7621  remulext2  7844  mulext1  7856  apmul1  8020  nnge1  8206  0mnnnnn0  8464  nn0lt2  8587  zneo  8606  uzind2  8617  fzind  8620  nn0ind-raph  8622  ledivge1le  8961  elfzmlbp  9297  difelfznle  9300  elfzodifsumelfzo  9364  ssfzo12  9387  flqeqceilz  9477  addmodlteq  9557  uzsinds  9595  facdiv  9839  facwordi  9841  bcpasc  9867  addcn2  10375  mulcn2  10377  climrecvg1n  10411  odd2np1  10505  oddge22np1  10513  gcdaddm  10607  algcvgblem  10663  cncongr1  10717
 Copyright terms: Public domain W3C validator