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

Theorem sylanbrc 645
Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylanbrc.1 (φψ)
sylanbrc.2 (φχ)
sylanbrc.3 (θ ↔ (ψ χ))
Assertion
Ref Expression
sylanbrc (φθ)

Proof of Theorem sylanbrc
StepHypRef Expression
1 sylanbrc.1 . . 3 (φψ)
2 sylanbrc.2 . . 3 (φχ)
31, 2jca 518 . 2 (φ → (ψ χ))
4 sylanbrc.3 . 2 (θ ↔ (ψ χ))
53, 4sylibr 203 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358
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  df-an 360
This theorem is referenced by:  ecase23d  1285  sbequ1  1918  sb2  2023  sbn  2062  eqeu  3007  euind  3023  reuind  3039  eqssd  3289  ssrabdv  3345  psstr  3373  vfinnc  4471  nnpw1ex  4484  evenoddnnnul  4514  sfinltfin  4535  sfin111  4536  imainss  5042  ssdmrn  5099  fnprg  5153  fnco  5191  f00  5249  f1ss  5262  f1f1orn  5297  foimacnv  5303  fun11iun  5305  dff3  5420  foco2  5426  ffnfv  5427  ffvresb  5431  isoini2  5498  f1oiso  5499  fnoprabg  5585  fmpt  5692  fmpt2d  5695  f1od  5726  sod  5937  so0  5941  iserd  5942  enpw1  6062  ncspw1eu  6159  ltcpw1pwg  6202  nchoicelem17  6305  nchoice  6308  fnfrec  6320
  Copyright terms: Public domain W3C validator