New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3bitr3i | GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 | ⊢ (φ ↔ ψ) |
3bitr3i.2 | ⊢ (φ ↔ χ) |
3bitr3i.3 | ⊢ (ψ ↔ θ) |
Ref | Expression |
---|---|
3bitr3i | ⊢ (χ ↔ θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.2 | . . 3 ⊢ (φ ↔ χ) | |
2 | 3bitr3i.1 | . . 3 ⊢ (φ ↔ ψ) | |
3 | 1, 2 | bitr3i 242 | . 2 ⊢ (χ ↔ ψ) |
4 | 3bitr3i.3 | . 2 ⊢ (ψ ↔ θ) | |
5 | 3, 4 | bitri 240 | 1 ⊢ (χ ↔ θ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 |
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 177 |
This theorem is referenced by: an12 772 cadan 1392 19.35 1600 cbval2 2004 cbvex2 2005 sbco2d 2087 equsb3 2102 elsb3 2103 elsb4 2104 sbcom2 2114 dfsb7 2119 sb7f 2120 eq2tri 2412 eqsb3 2454 clelsb3 2455 r19.35 2758 ralcom4 2877 rexcom4 2878 ceqsralt 2882 gencbvex 2901 gencbval 2903 ceqsrexbv 2973 euind 3023 reuind 3039 sbccomlem 3116 sbccom 3117 ab0 3569 difcom 3634 uniintsn 3963 pw1in 4164 dfimak2 4298 addcass 4415 elswap 4740 elxp2 4802 eqbrriv 4851 opelcnv 4893 dm0rn0 4921 opelres 4950 rninxp 5060 fununi 5160 dfoprab2 5558 opsnelsi 5774 oteltxp 5782 funsex 5828 pw1fnex 5852 brpw1fn 5854 nenpw1pwlem1 6084 lecex 6115 el2c 6191 brtcfn 6246 |
Copyright terms: Public domain | W3C validator |