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

Theorem syl5bir 146
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bir.1 (𝜓𝜑)
syl5bir.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bir (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3 (𝜓𝜑)
21biimpri 128 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 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:  3imtr3g  197  19.37-1  1580  mo3h  1969  necon1bidc  2272  necon4aidc  2288  ceqex  2694  ssdisj  3305  ralidm  3349  rexxfrd  4223  sucprcreg  4301  imain  5009  funopfv  5241  mpteqb  5289  funfvima  5418  fliftfun  5464  iinerm  6209  eroveu  6228  th3qlem1  6239  elni2  6470  genpdisj  6679  lttri3  7157  cau3lem  9941  climcau  10097
  Copyright terms: Public domain W3C validator