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 265 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 1, 2, 3 | 3anbi123d 1438 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3anbi3d 1444 ax12wdemo 2135 f1dom3el3dif 7078 frrlem1 8024 frrlem13 8036 wfrlem1 8051 wfrlem3a 8054 wfrlem15 8066 cofsmo 9880 axdc3lem3 10063 axdc3lem4 10064 iscatd2 17181 psgnunilem1 18882 nn0gsumfz 19366 opprsubrg 19818 lsspropd 20051 mdetunilem3 21508 mdetunilem9 21514 smadiadetr 21569 lmres 22194 cnhaus 22248 regsep2 22270 dishaus 22276 ordthauslem 22277 nconnsubb 22317 pthaus 22532 txhaus 22541 xkohaus 22547 regr1lem 22633 ustval 23097 methaus 23415 metnrmlem3 23755 pmltpclem1 24342 axtgeucl 26560 iscgrad 26899 dfcgra2 26918 f1otrge 26960 axeuclidlem 27050 umgrvad2edg 27298 elwspths2spth 28048 upgr3v3e3cycl 28260 upgr4cycl4dv4e 28265 vdgn1frgrv2 28376 numclwlk1lem1 28449 ex-opab 28512 isnvlem 28688 ajval 28939 adjeu 29967 adjval 29968 adj1 30011 adjeq 30013 cnlnssadj 30158 br8d 30666 lt2addrd 30791 xlt2addrd 30798 measval 31875 loop1cycl 32809 br8 33439 br6 33440 br4 33441 xpord2lem 33523 xpord3lem 33529 brsslt 33714 brcgr3 34082 brsegle 34144 fvray 34177 linedegen 34179 fvline 34180 poimirlem28 35540 isopos 36929 hlsuprexch 37130 2llnjN 37316 2lplnj 37369 cdlemk42 38690 zindbi 40469 jm2.27 40531 stoweidlem43 43257 fourierdlem42 43363 ichexmpl1 44592 sepfsepc 45892 iscnrm3rlem8 45912 iscnrm3llem2 45915 |
Copyright terms: Public domain | W3C validator |