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

Theorem syl5bir 142
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 124 . 2 (φψ)
3 syl5bir.2 . 2 (χ → (ψθ))
42, 3syl5 28 1 (χ → (φθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr3g  193  19.37-1  1561  mo3h  1950  necon1bidc  2251  necon4aidc  2267  ceqex  2665  ssdisj  3271  ralidm  3315  rexxfrd  4161  sucprcreg  4227  imain  4924  funopfv  5156  mpteqb  5204  funfvima  5333  fliftfun  5379  iinerm  6114  eroveu  6133  th3qlem1  6144  elni2  6298  genpdisj  6506  lttri3  6895
  Copyright terms: Public domain W3C validator