Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitrd | GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
Ref | Expression |
---|---|
3bitrd.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitrd.2 | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
3bitrd.3 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitrd | ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitrd.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 3bitrd.2 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | |
3 | 1, 2 | bitrd 187 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3bitrd.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 187 | 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: sbceqal 2936 sbcnel12g 2990 elxp4 4996 elxp5 4997 f1eq123d 5330 foeq123d 5331 f1oeq123d 5332 ofrfval 5958 eloprabi 6062 fnmpoovd 6080 smoeq 6155 ecidg 6461 ixpsnval 6563 enqbreq2 7133 ltanqg 7176 caucvgprprlemexb 7483 caucvgsrlemgt1 7571 caucvgsrlemoffres 7576 ltrennb 7630 apneg 8341 mulext1 8342 apdivmuld 8541 ltdiv23 8618 lediv23 8619 halfpos 8919 addltmul 8924 div4p1lem1div2 8941 ztri3or 9065 supminfex 9360 iccf1o 9755 fzshftral 9856 fzoshftral 9983 2tnp1ge0ge0 10042 fihashen1 10513 seq3coll 10553 cjap 10646 negfi 10967 tanaddaplem 11372 dvdssub 11465 addmodlteqALT 11484 dvdsmod 11487 oddp1even 11500 nn0o1gt2 11529 nn0oddm1d2 11533 infssuzex 11569 cncongr1 11711 cncongr2 11712 elmopn 12542 metss 12590 comet 12595 xmetxp 12603 limcmpted 12728 cnlimc 12737 |
Copyright terms: Public domain | W3C validator |