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

Theorem syl6rbbr 255
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1 (φ → (ψχ))
syl6rbbr.2 (θχ)
Assertion
Ref Expression
syl6rbbr (φ → (θψ))

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2 (φ → (ψχ))
2 syl6rbbr.2 . . 3 (θχ)
32bicomi 193 . 2 (χθ)
41, 3syl6rbb 253 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:  baib  871  reu8  3032  sbc6g  3071  r19.28z  3642  r19.28zv  3645  r19.37zv  3646  r19.45zv  3647  r19.27z  3648  r19.27zv  3649  r19.36zv  3650  ralidm  3653  ralsns  3763  rexsns  3764  ssunsn2  3865  iunconst  3977  iinconst  3978  ssofss  4076  snelpwg  4114  opres  4978  cores  5084  funssres  5144  fncnv  5158  dff1o5  5295  fvres  5342  funimass4  5368  dffo3  5422  funfvima  5459  eloprabga  5578  eqncg  6126  ncseqnc  6128  eqtc  6161  tcfnex  6244  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306  canncb  6332
 Copyright terms: Public domain W3C validator