![]() |
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 473 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | anbi12d 473 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 980 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 980 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 223 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3anbi12d 1313 3anbi13d 1314 3anbi23d 1315 limeq 4377 smoeq 6290 tfrlemi1 6332 tfr1onlemaccex 6348 tfrcllemaccex 6361 ereq1 6541 updjud 7080 ctssdclemr 7110 tapeq1 7250 tapeq2 7251 elinp 7472 sup3exmid 8913 iccshftr 9993 iccshftl 9995 iccdil 9997 icccntr 9999 fzaddel 10058 elfzomelpfzo 10230 seq3f1olemstep 10500 seq3f1olemp 10501 sumeq1 11362 summodclem2 11389 summodc 11390 zsumdc 11391 prodmodclem2 11584 prodmodc 11585 divalglemnn 11922 divalglemeunn 11925 divalglemeuneg 11927 dfgcd2 12014 pythagtriplem18 12280 pythagtriplem19 12281 ctiunct 12440 ssomct 12445 isstruct2im 12471 isstruct2r 12472 ptex 12712 isringd 13218 issubrg3 13373 fiinopn 13440 lmfval 13628 upxp 13708 2irrexpqap 14332 dceqnconst 14743 dcapnconst 14744 |
Copyright terms: Public domain | W3C validator |