Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5bbr | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5bbr.1 | ⊢ (𝜓 ↔ 𝜑) |
syl5bbr.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5bbr | ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5bbr.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 123 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | syl5bbr.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | syl5bb 181 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3bitr3g 211 ianordc 799 19.16 1447 19.19 1556 cbvab 2160 necon1bbiidc 2266 elabgt 2684 sbceq1a 2773 sbcralt 2834 sbcrext 2835 sbccsbg 2878 sbccsb2g 2879 iunpw 4211 tfis 4306 xp11m 4759 ressn 4858 fnssresb 5011 fun11iun 5147 funimass4 5224 dffo4 5315 f1ompt 5320 fliftf 5439 resoprab2 5598 ralrnmpt2 5615 rexrnmpt2 5616 1stconst 5842 2ndconst 5843 dfsmo2 5902 smoiso 5917 brecop 6196 ac6sfi 6352 prarloclemn 6597 axcaucvglemres 6973 reapti 7570 indstr 8536 iccneg 8857 sqap0 9320 sqrt00 9638 |
Copyright terms: Public domain | W3C validator |