Theorem 3anbi3i 1255

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
3anbi3i	|- ( ( ch /\ th /\ ph ) <-> ( ch /\ th /\ ps ) )

Proof of Theorem 3anbi3i

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

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:  cadcomb  1552  dfer2  7743  axgroth2  9647  oppgsubm  17792  xrsdsreclb  19793  ordthaus  21188  qtopeu  21519  regr1lem2  21543  isfbas2  21639  isclmp  22897  umgr2edg1  26103  xrge0adddir  29692  isros  30231  bnj964  31013  bnj1033  31037  dfon2lem7  31694  outsideofcom  32235  linecom  32257  linerflx2  32258  topdifinffinlem  33195  rdgeqoa  33218  ishlat2  34640  lhpex2leN  35299  lmbr3v  39977  lmbr3  39979  fourierdlem103  40426  fourierdlem104  40427  issmf  40937  issmff  40943  issmfle  40954  issmfgt  40965  issmfge  40978