Theorem 3anbi3i 1155

Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
3anbi3i	⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Proof of Theorem 3anbi3i

Step	Hyp	Ref	Expression
1		biid 263	. 2 ⊢ (𝜒 ↔ 𝜒)
2		biid 263	. 2 ⊢ (𝜃 ↔ 𝜃)
3		3anbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	1, 2, 3	3anbi123i 1151	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  cadcomb  1614  dfer2  8290  axgroth2  10247  oppgsubm  18490  xrsdsreclb  20592  ordthaus  21992  qtopeu  22324  regr1lem2  22348  isfbas2  22443  isclmp  23701  umgr2edg1  26993  xrge0adddir  30679  isros  31427  bnj964  32215  bnj1033  32241  cusgr3cyclex  32383  dfon2lem7  33034  outsideofcom  33589  linecom  33611  linerflx2  33612  topdifinffinlem  34631  rdgeqoa  34654  ishlat2  36504  lhpex2leN  37164  lmbr3v  42046  lmbr3  42048  fourierdlem103  42514  fourierdlem104  42515  issmf  43025  issmff  43031  issmfle  43042  issmfgt  43053  issmfge  43066