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

Theorem syl6rbbr 188
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 123 . 2 (𝜒𝜃)
41, 3syl6rbb 186 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:  imimorbdc  795  baib  828  pm5.6dc  835  xornbidc  1282  mo2dc  1955  reu8  2737  sbc6g  2788  r19.28m  3311  r19.45mv  3315  r19.27m  3316  ralsnsg  3407  ralsns  3408  rexsnsOLD  3410  iunconstm  3665  iinconstm  3666  unisucg  4151  funssres  4942  fncnv  4965  dff1o5  5135  funimass4  5224  fneqeql2  5276  fnniniseg2  5290  rexsupp  5291  unpreima  5292  dffo3  5314  funfvima  5390  dff13  5407  f1eqcocnv  5431  fliftf  5439  isocnv2  5452  eloprabga  5591  mpt22eqb  5610  opabex3d  5748  opabex3  5749  elxp6  5796  elxp7  5797  genpdflem  6605  ltnqpr  6691  ltexprlemloc  6705  xrlenlt  7084  negcon2  7264  elznn  8261  zq  8561  rpnegap  8615  shftdm  9423  rexanuz2  9589
  Copyright terms: Public domain W3C validator