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

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

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2 (φ → (ψχ))
2 syl6bbr.2 . . 3 (θχ)
32bicomi 123 . 2 (χθ)
41, 3syl6bb 185 1 (φ → (ψθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3bitr4g  212  bibi2i  216  equsalh  1596  eueq3dc  2692  sbcel12g  2842  sbceqg  2843  sbcnel12g  2844  reldisj  3248  r19.3rmOLD  3287  r19.3rm  3289  rabxp  4307  elrng  4453  iss  4581  eliniseg  4622  fcnvres  4998  dffv3g  5099  funimass4  5149  fndmdif  5197  fneqeql  5200  funimass3  5208  elrnrexdmb  5232  dff4im  5238  fconst4m  5306  elunirn  5330  riota1  5410  riota2df  5412  f1ocnvfv3  5425  eqfnov  5530  caoftrn  5659  mpt2xopovel  5778  rntpos  5794  ordgt0ge1  5933  iinerm  6089  erinxp  6091  qliftfun  6099  genpdflem  6361  genpdisj  6378  genpassl  6379  genpassu  6380  ltpopr  6432  ltexprlemm  6437  ltexprlemdisj  6443  ltexprlemloc  6444  letr  6699  bj-sseq  7038
  Copyright terms: Public domain W3C validator