Theorem 3anbi3d 1329

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		biidd 172	. 2 |- ( ph -> ( th <-> th ) )
2		3anbi1d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	3anbi13d 1325	1 |- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  ceqsex3v  2802  ceqsex4v  2803  ceqsex8v  2805  vtocl3gaf  2829  mob  2942  ordsoexmid  4594  tfr1onlemaccex  6401  tfrcllemaccex  6414  fseq1m1p1  10161  summodc  11526  fsum3  11530  divalglemnn  12059  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  mhmlem  13184  ring1  13555  lmodlema  13788  ivthreinc  14799