Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl5rbb | Structured version Visualization version GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
Ref | Expression |
---|---|
syl5rbb.1 | ⊢ (𝜑 ↔ 𝜓) |
syl5rbb.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5rbb | ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | syl5rbb.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | syl5bb 285 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
4 | 3 | bicomd 225 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: syl5rbbr 288 necon1abid 3052 necon4abid 3054 uniiunlem 4059 r19.9rzv 4443 2reu4lem 4463 inimasn 6006 fnresdisj 6460 f1oiso 7096 reldm 7735 rdglim2 8060 mptelixpg 8491 1idpr 10443 nndiv 11675 fz1sbc 12975 grpid 18131 znleval 20693 fbunfip 22469 lmflf 22605 metcld2 23902 lgsne0 25903 isuvtx 27169 loopclwwlkn1b 27812 clwwlknun 27883 frgrncvvdeqlem2 28071 isph 28591 ofpreima 30402 eulerpartlemd 31617 bnj168 31993 opelco3 33011 wl-2sb6d 34786 poimirlem26 34910 cnambfre 34932 heibor1 35080 opltn0 36318 cvrnbtwn2 36403 cvrnbtwn4 36407 atlltn0 36434 pmapjat1 36981 dih1dimatlem 38457 2rexfrabdioph 39384 dnwech 39639 rfovcnvf1od 40341 uneqsn 40364 lighneallem2 43762 isrnghm 44154 rnghmval2 44157 |
Copyright terms: Public domain | W3C validator |