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

Theorem syl5bir 151
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 131 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr3g  202  19.37-1  1607  mo3h  1998  necon1bidc  2303  necon4aidc  2319  ceqex  2735  ssdisj  3327  ralidm  3369  rexxfrd  4258  sucprcreg  4337  imain  5058  f0rn0  5162  funopfv  5301  mpteqb  5350  funfvima  5481  fliftfun  5530  iinerm  6310  eroveu  6329  th3qlem1  6340  updjudhf  6707  elni2  6810  genpdisj  7019  lttri3  7502  zfz1iso  10135  cau3lem  10435  maxleast  10534  rexanre  10541  climcau  10619  isummo  10655  divgcdcoprmex  10951  prmind2  10969
  Copyright terms: Public domain W3C validator