![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3id | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3id.1 | ⊢ (𝜓 ↔ 𝜑) |
bitr3id.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
bitr3id | ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3id.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 131 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | bitr3id.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | syl5bb 191 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3bitr3g 221 ianordc 885 19.16 1532 19.19 1643 cbvab 2278 necon1bbiidc 2385 rspc2gv 2825 elabgt 2849 sbceq1a 2942 sbcralt 3009 sbcrext 3010 sbccsbg 3056 sbccsb2g 3057 iunpw 4434 tfis 4536 xp11m 5017 ressn 5119 fnssresb 5275 fun11iun 5428 funimass4 5512 dffo4 5608 f1ompt 5611 fliftf 5740 resoprab2 5908 ralrnmpo 5925 rexrnmpo 5926 1stconst 6158 2ndconst 6159 dfsmo2 6224 smoiso 6239 brecop 6559 ixpsnf1o 6670 ac6sfi 6832 ismkvnex 7077 prarloclemn 7398 axcaucvglemres 7798 reapti 8433 indstr 9483 iccneg 9871 sqap0 10463 sqrt00 10917 minclpr 11113 fprodseq 11457 absefib 11644 efieq1re 11645 prmind2 11968 sincosq3sgn 13088 sincosq4sgn 13089 pw1nct 13514 iswomninnlem 13561 |
Copyright terms: Public domain | W3C validator |