Theorem 3anbi1d 1403

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

Hypothesis

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

Assertion

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

Proof of Theorem 3anbi1d

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

Syntax hints:   -> wi 4   <-> 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:  vtocl3gaf  3275  axdc4uz  12783  wrdl3s3  13705  relexpindlem  13803  sqrtval  13977  sqreu  14100  coprmprod  15375  mreexexd  16308  mreexexdOLD  16309  iscatd2  16342  lmodprop2d  18925  neiptopnei  20936  hausnei  21132  isreg2  21181  regr1lem2  21543  ustval  22006  ustuqtop4  22048  axtgupdim2  25370  axtgeucl  25371  iscgra  25701  brbtwn  25779  ax5seg  25818  axlowdim  25841  axeuclidlem  25842  wlkonprop  26554  upgr2wlk  26564  upgrf1istrl  26600  elwspths2spth  26862  clwlkclwwlk  26903  upgr4cycl4dv4e  27045  extwwlkfab  27223  nvi  27469  br8d  29422  xlt2addrd  29523  isslmd  29755  slmdlema  29756  tgoldbachgt  30741  axtgupdim2OLD  30746  br8  31646  br6  31647  br4  31648  fvtransport  32139  brcolinear2  32165  colineardim1  32168  fscgr  32187  idinside  32191  brsegle  32215  poimirlem28  33437  caures  33556  iscringd  33797  oposlem  34469  cdleme18d  35582  jm2.27  37575  9gbo  41662  11gbo  41663