MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbbr Structured version   Visualization version   GIF version

Theorem sylbbr 226
Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 207, sylib 208, sylbir 225, sylibr 224; four inferences inferring an implication from two biconditionals: sylbb 209, sylbbr 226, sylbb1 227, sylbb2 228; four inferences inferring a biconditional from two biconditionals: bitri 264, bitr2i 265, bitr3i 266, bitr4i 267 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 222, bitrd 268, syl5bb 272, syl6bb 276 and variants. (Contributed by BJ, 21-Apr-2019.)

Hypotheses
Ref Expression
sylbbr.1 (𝜑𝜓)
sylbbr.2 (𝜓𝜒)
Assertion
Ref Expression
sylbbr (𝜒𝜑)

Proof of Theorem sylbbr
StepHypRef Expression
1 sylbbr.2 . . 3 (𝜓𝜒)
21biimpri 218 . 2 (𝜒𝜓)
3 sylbbr.1 . 2 (𝜑𝜓)
42, 3sylibr 224 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  bitri  264  euelss  3947  dfnfc2  4486  ndmima  5537  axcclem  9317  fsumcom2  14549  fprodcom2  14758  pmtr3ncomlem1  17939  mdetunilem7  20472  cmpcov2  21241  umgredg  26078  vtxdginducedm1  26495  2pthfrgrrn  27262  conway  32035  f1omptsnlem  33313  igenval2  33995  mpt2bi123f  34101  brtrclfv2  38336  clsk1indlem3  38658
  Copyright terms: Public domain W3C validator