Theorem 3anbi1i 1198

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

Hypothesis

Ref	Expression
3anbi1i.1	|- ( ph <-> ps )

Assertion

Ref	Expression
3anbi1i	|- ( ( ph /\ ch /\ th ) <-> ( ps /\ ch /\ th ) )

Proof of Theorem 3anbi1i

Step	Hyp	Ref	Expression
1		3anbi1i.1	. 2 |- ( ph <-> ps )
2		biid 240	. 2 |- ( ch <-> ch )
3		biid 240	. 2 |- ( th <-> th )
4	1, 2, 3	3anbi123i 1196	1 |- ( ( ph /\ ch /\ th ) <-> ( ps /\ ch /\ th ) )

Syntax hints:   <-> wb 188   /\ w3a 984

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 189  df-an 373  df-3an 986

This theorem is referenced by:  iinfi  7928  fzolb  11923  brfi1uzind  12648  opfi1uzind  12651  sqrlem5  13303  bitsmod  14403  isfunc  15762  txcn  20634  trfil2  20895  eulerpartlemn  29207  bnj976  29582  bnj543  29697  bnj594  29716  bnj917  29738  topdifinffinlem  31743  dath  33295  elfzolborelfzop1  40303  nnolog2flm1  40388