Theorem 3anbi3d 1331

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

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

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 983

This theorem is referenced by:  ceqsex3v  2815  ceqsex4v  2816  ceqsex8v  2818  vtocl3gaf  2842  mob  2955  ordsoexmid  4611  tfr1onlemaccex  6436  tfrcllemaccex  6449  fseq1m1p1  10219  pfxsuff1eqwrdeq  11153  summodc  11727  fsum3  11731  divalglemnn  12262  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  mhmlem  13483  ring1  13854  lmodlema  14087  ivthreinc  15150  dvmptfsum  15230