![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi3i | Structured version Visualization version GIF version |
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi1i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
3anbi3i | ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 251 | . 2 ⊢ (𝜒 ↔ 𝜒) | |
2 | biid 251 | . 2 ⊢ (𝜃 ↔ 𝜃) | |
3 | 3anbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
4 | 1, 2, 3 | 3anbi123i 1159 | 1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: cadcomb 1699 dfer2 7910 axgroth2 9837 oppgsubm 17990 xrsdsreclb 19993 ordthaus 21388 qtopeu 21719 regr1lem2 21743 isfbas2 21838 isclmp 23095 umgr2edg1 26300 xrge0adddir 29999 isros 30538 bnj964 31318 bnj1033 31342 dfon2lem7 31997 outsideofcom 32539 linecom 32561 linerflx2 32562 topdifinffinlem 33504 rdgeqoa 33527 ishlat2 35141 lhpex2leN 35800 lmbr3v 40478 lmbr3 40480 fourierdlem103 40927 fourierdlem104 40928 issmf 41441 issmff 41447 issmfle 41458 issmfgt 41469 issmfge 41482 |
Copyright terms: Public domain | W3C validator |