| 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 2979 necon4abid 2981 uniiunlem 4087 r19.9rzv 4500 2reu4lem 4522 intprg 4981 inimasn 6176 fnresdisj 6688 fnsnfv 6988 f1oiso 7371 reldm 8069 rdglim2 8472 mptelixpg 8975 1idpr 11069 nndiv 12312 fz1sbc 13640 grpid 18993 isrnghm 20441 rnghmval2 20444 znleval 21573 fbunfip 23877 lmflf 24013 metcld2 25341 lgsne0 27379 isuvtx 29412 loopclwwlkn1b 30061 clwwlknun 30131 frgrncvvdeqlem2 30319 isph 30841 ofpreima 32675 fdifsupp 32694 ressply1mon1p 33593 eulerpartlemd 34368 bnj168 34744 cardpred 35104 opelco3 35775 wl-2sb6d 37559 poimirlem26 37653 cnambfre 37675 heibor1 37817 opltn0 39191 cvrnbtwn2 39276 cvrnbtwn4 39280 atlltn0 39307 pmapjat1 39855 dih1dimatlem 41331 2rexfrabdioph 42807 dnwech 43060 rfovcnvf1od 44017 uneqsn 44038 lighneallem2 47593 stgredgiun 47925 |
| Copyright terms: Public domain | W3C validator |