![]() |
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 260 | . 2 ⊢ (𝜒 ↔ 𝜒) | |
2 | biid 260 | . 2 ⊢ (𝜃 ↔ 𝜃) | |
3 | 3anbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
4 | 1, 2, 3 | 3anbi123i 1152 | 1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: cadcomb 1607 dfwrecsOLD 8328 dfer2 8735 ttrclresv 9760 axgroth2 10868 oppgsubm 19359 xrsdsreclb 21410 ordthaus 23379 qtopeu 23711 regr1lem2 23735 isfbas2 23830 isclmp 25115 umgr2edg1 29147 xrge0adddir 32901 isros 34001 bnj964 34788 bnj1033 34814 cusgr3cyclex 34964 dfon2lem7 35613 outsideofcom 35952 linecom 35974 linerflx2 35975 topdifinffinlem 37054 rdgeqoa 37077 ishlat2 39051 lhpex2leN 39712 aks6d1c1rh 41823 sn-isghm 42327 lmbr3v 45366 lmbr3 45368 fourierdlem103 45830 fourierdlem104 45831 issmf 46349 issmff 46355 issmfle 46366 issmfgt 46377 issmfge 46391 funcf2lem 48339 |
Copyright terms: Public domain | W3C validator |