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

Theorem syl5rbb 271
Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)
Hypotheses
Ref Expression
syl5rbb.1 (𝜑𝜓)
syl5rbb.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5rbb (𝜒 → (𝜃𝜑))

Proof of Theorem syl5rbb
StepHypRef Expression
1 syl5rbb.1 . . 3 (𝜑𝜓)
2 syl5rbb.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5bb 270 . 2 (𝜒 → (𝜑𝜃))
43bicomd 211 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  syl5rbbr  273  necon1abid  2819  necon4abid  2821  uniiunlem  3652  r19.9rzv  4016  inimasn  5454  fnresdisj  5900  f1oiso  6478  reldm  7087  rdglim2  7392  mptelixpg  7808  1idpr  9707  nndiv  10910  fz1sbc  12242  grpid  17228  znleval  19669  fbunfip  21430  lmflf  21566  metcld2  22857  lgsne0  24804  isph  26854  ofpreima  28641  eulerpartlemd  29548  bnj168  29845  opelco3  30716  wl-2sb6d  32303  poimirlem26  32388  cnambfre  32411  heibor1  32562  opltn0  33278  cvrnbtwn2  33363  cvrnbtwn4  33367  atlltn0  33394  pmapjat1  33940  dih1dimatlem  35419  2rexfrabdioph  36161  dnwech  36419  rfovcnvf1od  37101  uneqsn  37124  csbabgOLD  37855  2reu4a  39621  lighneallem2  39845  isuvtxa  40602  clwwlksnun  41262  isrnghm  41663  rnghmval2  41666
  Copyright terms: Public domain W3C validator