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  1546  mo3h  1935  necon1bidc  2235  necon4aidc  2251  ceqex  2648  ssdisj  3254  ralidm  3300  rexxfrd  4145  sucprcreg  4211  imain  4907  funopfv  5138  mpteqb  5186  funfvima  5315  fliftfun  5361  iinerm  6089  eroveu  6108  th3qlem1  6119  elni2  6174  genpdisj  6378
  Copyright terms: Public domain W3C validator