![]() |
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 253 | . 2 ⊢ (𝜒 ↔ 𝜒) | |
2 | biid 253 | . 2 ⊢ (𝜃 ↔ 𝜃) | |
3 | 3anbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
4 | 1, 2, 3 | 3anbi123i 1195 | 1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ w3a 1108 |
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 386 df-3an 1110 |
This theorem is referenced by: cadcomb 1723 dfer2 7983 axgroth2 9935 oppgsubm 18104 xrsdsreclb 20115 ordthaus 21517 qtopeu 21848 regr1lem2 21872 isfbas2 21967 isclmp 23224 umgr2edg1 26444 xrge0adddir 30208 isros 30747 bnj964 31530 bnj1033 31554 dfon2lem7 32206 outsideofcom 32748 linecom 32770 linerflx2 32771 topdifinffinlem 33693 rdgeqoa 33716 ishlat2 35374 lhpex2leN 36034 lmbr3v 40721 lmbr3 40723 fourierdlem103 41169 fourierdlem104 41170 issmf 41683 issmff 41689 issmfle 41700 issmfgt 41711 issmfge 41724 |
Copyright terms: Public domain | W3C validator |