![]() |
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 222 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: bitr3di 286 necon1abid 2978 necon4abid 2980 uniiunlem 4084 r19.9rzv 4499 2reu4lem 4525 intprg 4985 inimasn 6155 fnresdisj 6670 fnsnfv 6970 f1oiso 7351 reldm 8034 rdglim2 8438 mptelixpg 8935 1idpr 11030 nndiv 12265 fz1sbc 13584 grpid 18903 isrnghm 20339 rnghmval2 20342 znleval 21421 fbunfip 23694 lmflf 23830 metcld2 25156 lgsne0 27183 isuvtx 29087 loopclwwlkn1b 29730 clwwlknun 29800 frgrncvvdeqlem2 29988 isph 30510 ofpreima 32325 ressply1mon1p 33099 eulerpartlemd 33831 bnj168 34207 cardpred 34559 opelco3 35218 wl-2sb6d 36890 poimirlem26 36981 cnambfre 37003 heibor1 37145 opltn0 38527 cvrnbtwn2 38612 cvrnbtwn4 38616 atlltn0 38643 pmapjat1 39191 dih1dimatlem 40667 2rexfrabdioph 42000 dnwech 42256 rfovcnvf1od 43221 uneqsn 43242 lighneallem2 46736 |
Copyright terms: Public domain | W3C validator |