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  2820  ceqsex4v  2821  ceqsex8v  2823  vtocl3gaf  2847  mob  2962  ordsoexmid  4628  tfr1onlemaccex  6457  tfrcllemaccex  6470  fseq1m1p1  10252  pfxsuff1eqwrdeq  11190  summodc  11809  fsum3  11813  divalglemnn  12344  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  mhmlem  13565  ring1  13936  lmodlema  14169  ivthreinc  15232  dvmptfsum  15312