Theorem 3anbi1i 1253

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 251	. 2 |- ( ch <-> ch )
3		biid 251	. 2 |- ( th <-> th )
4	1, 2, 3	3anbi123i 1251	1 |- ( ( ph /\ ch /\ th ) <-> ( ps /\ ch /\ th ) )

Syntax hints:   <-> wb 196   /\ w3a 1037

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 386  df-3an 1039

This theorem is referenced by:  iinfi  8323  fzolb  12476  brfi1uzind  13280  opfi1uzind  13283  brfi1uzindOLD  13286  opfi1uzindOLD  13289  sqrlem5  13987  bitsmod  15158  isfunc  16524  txcn  21429  trfil2  21691  isclmp  22897  eulerpartlemn  30443  bnj976  30848  bnj543  30963  bnj594  30982  bnj917  31004  topdifinffinlem  33195  dath  35022  elfzolborelfzop1  42309  nnolog2flm1  42384