Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3anbi123d | GIF version |
Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.) |
Ref | Expression |
---|---|
bi3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bi3d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
bi3d.3 | ⊢ (𝜑 → (𝜂 ↔ 𝜁)) |
Ref | Expression |
---|---|
3anbi123d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi3d.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bi3d.2 | . . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
3 | 1, 2 | anbi12d 464 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | anbi12d 464 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 949 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 949 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 222 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 947 |
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 df-3an 949 |
This theorem is referenced by: 3anbi12d 1276 3anbi13d 1277 3anbi23d 1278 limeq 4269 smoeq 6155 tfrlemi1 6197 tfr1onlemaccex 6213 tfrcllemaccex 6226 ereq1 6404 updjud 6935 ctssdclemr 6965 elinp 7250 sup3exmid 8683 iccshftr 9745 iccshftl 9747 iccdil 9749 icccntr 9751 fzaddel 9807 elfzomelpfzo 9976 seq3f1olemstep 10242 seq3f1olemp 10243 sumeq1 11092 summodclem2 11119 summodc 11120 zsumdc 11121 divalglemnn 11542 divalglemeunn 11545 divalglemeuneg 11547 dfgcd2 11629 ctiunct 11880 isstruct2im 11896 isstruct2r 11897 fiinopn 12098 lmfval 12288 upxp 12368 |
Copyright terms: Public domain | W3C validator |