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

Theorem syl6rbbr 197
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 130 . 2 (𝜒𝜃)
41, 3syl6rbb 195 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imimorbdc  831  baib  864  pm5.6dc  871  xornbidc  1325  mo2dc  2000  reu8  2802  sbc6g  2853  dfss4st  3221  r19.28m  3358  r19.45mv  3362  r19.44mv  3363  r19.27m  3364  ralsnsg  3463  ralsns  3464  iunconstm  3721  iinconstm  3722  unisucg  4215  relsng  4509  funssres  5021  fncnv  5045  dff1o5  5225  funimass4  5318  fneqeql2  5371  fnniniseg2  5385  rexsupp  5386  unpreima  5387  dffo3  5409  funfvima  5487  dff13  5508  f1eqcocnv  5531  fliftf  5539  isocnv2  5552  eloprabga  5692  mpt22eqb  5711  opabex3d  5849  opabex3  5850  elxp6  5897  elxp7  5898  sbthlemi5  6614  sbthlemi6  6615  genpdflem  7010  ltnqpr  7096  ltexprlemloc  7110  xrlenlt  7495  negcon2  7679  dfinfre  8352  elznn  8699  zq  9043  rpnegap  9098  modqmuladdnn0  9703  shftdm  10152  rexfiuz  10317  rexanuz2  10319  odd2np1  10748  divalgb  10800  infssuzex  10820  isprm4  10976
  Copyright terms: Public domain W3C validator