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

Theorem sylbird 170
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 158 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 45 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
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:  3imtr3d  202  drex1  1798  eqreu  2931  onsucsssucr  4510  ordsucunielexmid  4532  ovi3  6013  tfrlem9  6322  dom2lem  6774  distrlem4prl  7585  distrlem4pru  7586  recexprlemm  7625  caucvgprlem1  7680  caucvgprprlemexb  7708  aptisr  7780  map2psrprg  7806  renegcl  8220  addid0  8332  remulext2  8559  mulext1  8571  apmul1  8747  nnge1  8944  0mnnnnn0  9210  nn0lt2  9336  zneo  9356  uzind2  9367  fzind  9370  nn0ind-raph  9372  ledivge1le  9728  elfzmlbp  10134  difelfznle  10137  elfzodifsumelfzo  10203  ssfzo12  10226  flqeqceilz  10320  addmodlteq  10400  uzsinds  10444  qsqeqor  10633  facdiv  10720  facwordi  10722  bcpasc  10748  addcn2  11320  mulcn2  11322  climrecvg1n  11358  odd2np1  11880  oddge22np1  11888  gcdaddm  11987  algcvgblem  12051  cncongr1  12105  pcdvdsb  12321  pcaddlem  12340  infpnlem1  12359  prmunb  12362  imasaddfnlemg  12740  subrgdvds  13361  aprcotr  13380  metss2lem  14082  lgseisenlem2  14536  2sqlem6  14552
  Copyright terms: Public domain W3C validator