![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi23d | Structured version Visualization version GIF version |
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi12d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3anbi12d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
3anbi23d | ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 254 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
2 | 3anbi12d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 1, 2, 3 | 3anbi123d 1416 | 1 ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1069 |
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 199 df-an 388 df-3an 1071 |
This theorem is referenced by: f1dom3el3dif 6850 wrecseq123 7749 oeeui 8027 fpwwe2lem5 9852 pwfseqlem4a 9879 pwfseqlem4 9880 swrdccatin12lem3 13931 prodeq2w 15124 prodeq2ii 15125 divalg 15612 dfgcd2 15748 iscatd2 16822 posi 17430 issubg3 18093 pmtrfrn 18359 psgnunilem2 18397 psgnunilem3 18398 lmhmpropd 19579 lbsacsbs 19662 frlmphl 20642 neiptoptop 21458 neiptopnei 21459 cnhaus 21681 nrmsep 21684 dishaus 21709 ordthauslem 21710 nconnsubb 21750 pthaus 21965 txhaus 21974 xkohaus 21980 regr1lem 22066 isust 22530 ustuqtop4 22571 methaus 22848 metnrmlem3 23187 iscau4 23600 pmltpclem1 23767 dvfsumlem2 24342 aannenlem1 24635 aannenlem2 24636 istrkgcb 25959 hlbtwn 26114 iscgra 26312 dfcgra2 26333 f1otrge 26376 axlowdim 26465 axeuclidlem 26466 eengtrkg 26490 clwwlk 27504 upgr3v3e3cycl 27724 upgr4cycl4dv4e 27729 numclwwlk5 27960 ex-opab 28004 l2p 28048 vciOLD 28130 isvclem 28146 isnvlem 28179 dipass 28414 adj1 29506 adjeq 29508 cnlnssadj 29653 br8d 30142 carsgmon 31249 carsgsigalem 31250 carsgclctunlem2 31254 carsgclctun 31256 bnj1154 31948 br8 32549 br6 32550 br4 32551 frecseq123 32677 brsslt 32812 fvtransport 33051 brcgr3 33065 brfs 33098 fscgr 33099 btwnconn1lem11 33116 brsegle 33127 fvray 33160 linedegen 33162 fvline 33163 poimirlem28 34398 poimirlem32 34402 heiborlem2 34569 hlsuprexch 35999 3dim1lem5 36084 lplni2 36155 2llnjN 36185 lvoli2 36199 2lplnj 36238 cdleme18d 36913 cdlemg1cex 37206 ismrc 38731 monotoddzzfi 38973 oddcomabszz 38975 zindbi 38977 rmydioph 39045 fsumiunss 41321 sumnnodd 41376 stoweidlem31 41781 stoweidlem34 41784 stoweidlem43 41793 stoweidlem48 41798 fourierdlem42 41899 sge0iunmptlemre 42162 sge0iunmpt 42165 vonioo 42429 vonicc 42432 |
Copyright terms: Public domain | W3C validator |