|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3anbi13d | 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 | 
|---|---|
| 3anbi13d | ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3anbi12d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | biidd 262 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
| 3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
| 4 | 1, 2, 3 | 3anbi123d 1437 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: 3anbi3d 1443 ax12wdemo 2134 f1dom3el3dif 7290 xpord2lem 8168 xpord3lem 8175 frrlem1 8312 frrlem13 8324 wfrlem1OLD 8349 wfrlem3OLDa 8352 wfrlem15OLD 8364 cofsmo 10310 axdc3lem3 10493 axdc3lem4 10494 iscatd2 17725 psgnunilem1 19512 nn0gsumfz 20003 opprsubrg 20594 lsspropd 21017 mdetunilem3 22621 mdetunilem9 22627 smadiadetr 22682 lmres 23309 cnhaus 23363 regsep2 23385 dishaus 23391 ordthauslem 23392 nconnsubb 23432 pthaus 23647 txhaus 23656 xkohaus 23662 regr1lem 23748 ustval 24212 methaus 24534 metnrmlem3 24884 pmltpclem1 25484 brsslt 27831 axtgeucl 28481 iscgrad 28820 dfcgra2 28839 f1otrge 28881 axeuclidlem 28978 umgrvad2edg 29231 elwspths2spth 29988 upgr3v3e3cycl 30200 upgr4cycl4dv4e 30205 vdgn1frgrv2 30316 numclwlk1lem1 30389 ex-opab 30452 isnvlem 30630 ajval 30881 adjeu 31909 adjval 31910 adj1 31953 adjeq 31955 cnlnssadj 32100 br8d 32623 lt2addrd 32756 xlt2addrd 32763 crngmxidl 33498 constrconj 33787 measval 34200 loop1cycl 35143 br8 35757 br6 35758 br4 35759 brcgr3 36048 brsegle 36110 fvray 36143 linedegen 36145 fvline 36146 poimirlem28 37656 isopos 39182 hlsuprexch 39384 2llnjN 39570 2lplnj 39623 cdlemk42 40944 zindbi 42963 jm2.27 43025 nnoeomeqom 43330 tfsconcatrev 43366 rp-brsslt 43441 stoweidlem43 46063 fourierdlem42 46169 ichexmpl1 47461 vopnbgrel 47845 dfclnbgr6 47847 dfnbgr6 47848 cycl3grtri 47919 grimgrtri 47921 usgrgrtrirex 47922 grlimgrtri 47968 usgrexmpl1tri 47989 sepfsepc 48832 iscnrm3rlem8 48851 iscnrm3llem2 48854 | 
| Copyright terms: Public domain | W3C validator |