| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bitr2id | Structured version Visualization version GIF version | ||
| Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
| Ref | Expression |
|---|---|
| bitr2id.1 | ⊢ (𝜑 ↔ 𝜓) |
| bitr2id.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
| Ref | Expression |
|---|---|
| bitr2id | ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr2id.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | bitr2id.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
| 3 | 1, 2 | bitrid 283 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
| 4 | 3 | bicomd 223 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: bitr3di 286 necon1abid 2968 necon4abid 2970 uniiunlem 4020 r19.9rzv 4435 2reu4lem 4453 intprg 4913 inimasn 6109 fnresdisj 6607 fnsnfv 6908 f1oiso 7295 reldm 7986 rdglim2 8360 mptelixpg 8872 1idpr 10941 nndiv 12212 fz1sbc 13543 grpid 18940 isrnghm 20410 rnghmval2 20413 znleval 21523 fbunfip 23822 lmflf 23958 metcld2 25262 lgsne0 27286 sltssnb 27749 isuvtx 29452 loopclwwlkn1b 30100 clwwlknun 30170 frgrncvvdeqlem2 30358 isph 30881 ofpreima 32726 fdifsupp 32746 ressply1mon1p 33616 eulerpartlemd 34498 bnj168 34861 cardpred 35223 opelco3 35945 qdiffALT 37630 wl-2sb6d 37871 poimirlem26 37955 cnambfre 37977 heibor1 38119 opltn0 39624 cvrnbtwn2 39709 cvrnbtwn4 39713 atlltn0 39740 pmapjat1 40287 dih1dimatlem 41763 2rexfrabdioph 43212 dnwech 43464 rfovcnvf1od 44419 uneqsn 44440 lighneallem2 48057 stgredgiun 48422 isinito2lem 49961 |
| Copyright terms: Public domain | W3C validator |