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