New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl5bir GIF version

Theorem syl5bir 209
 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 197 . 2 (φψ)
3 syl5bir.2 . 2 (χ → (ψθ))
42, 3syl5 28 1 (χ → (φθ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  3imtr3g  260  oplem1  930  nic-ax  1438  19.30  1604  19.33b  1608  ax10  1944  necon4bd  2578  ceqex  2969  ssdisj  3600  pssdifn0  3611  ltfintr  4459  evenodddisj  4516  sfinltfin  4535  fun11iun  5305  funopfv  5357  dff3  5420  funfvima  5459  trrd  5925  peano4nc  6150  ncspw1eu  6159  fce  6188
 Copyright terms: Public domain W3C validator