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

Theorem syl6rbbr 192
 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 127 . 2 (𝜒𝜃)
41, 3syl6rbb 190 1 (𝜑 → (𝜃𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  imimorbdc  806  baib  839  pm5.6dc  846  xornbidc  1298  mo2dc  1971  reu8  2759  sbc6g  2810  r19.28m  3338  r19.45mv  3342  r19.27m  3343  ralsnsg  3434  ralsns  3435  rexsnsOLD  3437  iunconstm  3692  iinconstm  3693  unisucg  4178  funssres  4969  fncnv  4992  dff1o5  5162  funimass4  5251  fneqeql2  5303  fnniniseg2  5317  rexsupp  5318  unpreima  5319  dffo3  5341  funfvima  5417  dff13  5434  f1eqcocnv  5458  fliftf  5466  isocnv2  5479  eloprabga  5618  mpt22eqb  5637  opabex3d  5775  opabex3  5776  elxp6  5823  elxp7  5824  genpdflem  6662  ltnqpr  6748  ltexprlemloc  6762  xrlenlt  7142  negcon2  7326  elznn  8317  zq  8657  rpnegap  8712  modqmuladdnn0  9317  shftdm  9650  rexfiuz  9815  rexanuz2  9817  odd2np1  10183
 Copyright terms: Public domain W3C validator