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

Theorem syl5bbr 250
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1 (ψφ)
syl5bbr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5bbr (χ → (φθ))

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3 (ψφ)
21bicomi 193 . 2 (φψ)
3 syl5bbr.2 . 2 (χ → (ψθ))
42, 3syl5bb 248 1 (χ → (φθ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1860  19.19  1862  sbco2  2086  cbvab  2471  necon1bbid  2570  necon4abid  2580  elabgt  2982  sbceq1a  3056  sbcralt  3118  sbccsbg  3164  sbccsb2g  3165  opkelimagekg  4271  vfin1cltv  4547  phialllem1  4616  phiall  4618  xp11  5056  nfunv  5138  fnssresb  5195  fun11iun  5305  dffo4  5423  elunirn  5470  isomin  5496  resoprab2  5582  nchoicelem11  6299
 Copyright terms: Public domain W3C validator