Theorem 3anbi3d 1318

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 1314	1 |- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )

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

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 980

This theorem is referenced by:  ceqsex3v  2777  ceqsex4v  2778  ceqsex8v  2780  vtocl3gaf  2804  mob  2917  ordsoexmid  4555  tfr1onlemaccex  6339  tfrcllemaccex  6352  fseq1m1p1  10063  summodc  11357  fsum3  11361  divalglemnn  11888  divalglemeunn  11891  divalglemex  11892  divalglemeuneg  11893  mhmlem  12837  ring1  13030