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

Theorem syl5rbb 272
 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 271 . 2 (𝜒 → (𝜑𝜃))
43bicomd 212 1 (𝜒 → (𝜃𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  syl5rbbr  274  necon1abid  2820  necon4abid  2822  uniiunlem  3653  r19.9rzv  4017  inimasn  5469  fnresdisj  5915  f1oiso  6501  reldm  7110  rdglim2  7415  mptelixpg  7831  1idpr  9730  nndiv  10938  fz1sbc  12285  grpid  17280  znleval  19722  fbunfip  21483  lmflf  21619  metcld2  22913  lgsne0  24860  isph  27061  ofpreima  28848  eulerpartlemd  29755  bnj168  30052  opelco3  30923  wl-2sb6d  32520  poimirlem26  32605  cnambfre  32628  heibor1  32779  opltn0  33495  cvrnbtwn2  33580  cvrnbtwn4  33584  atlltn0  33611  pmapjat1  34157  dih1dimatlem  35636  2rexfrabdioph  36378  dnwech  36636  rfovcnvf1od  37318  uneqsn  37341  csbabgOLD  38072  2reu4a  39838  lighneallem2  40061  isuvtxa  40621  clwwlksnun  41281  isrnghm  41682  rnghmval2  41685
 Copyright terms: Public domain W3C validator