Theorem 3anbi3d 1405

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 252	. 2 |- ( ph -> ( th <-> th ) )
2		3anbi1d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	3anbi13d 1401	1 |- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )

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:  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  vtocl3gaf  3275  mob  3388  offval22  7253  smogt  7464  cfsmolem  9092  fseq1m1p1  12415  2swrd1eqwrdeq  13454  2swrd2eqwrdeq  13696  wrdl3s3  13705  prodmo  14666  fprod  14671  divalg  15126  funcres2b  16557  posi  16950  mhmlem  17535  isdrngrd  18773  lmodlema  18868  connsub  21224  lmmbr3  23058  lmmcvg  23059  dvmptfsum  23738  axtg5seg  25364  axtgupdim2  25370  axtgeucl  25371  ishlg  25497  hlcomb  25498  brbtwn  25779  axlowdim  25841  axeuclidlem  25842  usgr2wlkspth  26655  usgr2pth0  26661  wwlksnwwlksnon  26810  umgrwwlks2on  26850  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  nvi  27469  isslmd  29755  slmdlema  29756  inelsros  30241  diffiunisros  30242  hgt749d  30727  tgoldbachgt  30741  axtgupdim2OLD  30746  afsval  30749  brafs  30750  bnj981  31020  bnj1326  31094  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3  31310  frrlem1  31780  noprefixmo  31848  nosupno  31849  nosupfv  31852  brofs  32112  brifs  32150  cgr3permute1  32155  brcolinear2  32165  colineardim1  32168  brfs  32186  btwnconn1  32208  brsegle  32215  unblimceq0  32498  unbdqndv2  32502  rdgeqoa  33218  iscringd  33797  oposlem  34469  ishlat1  34639  3dim1lem5  34752  lvoli2  34867  cdlemk42  36229  diclspsn  36483  monotoddzz  37508  jm2.27  37575  mendlmod  37763  fiiuncl  39234  wessf1ornlem  39371  infleinf  39588  fmulcl  39813  fmuldfeqlem1  39814  fmuldfeq  39815  climinf2mpt  39946  climinfmpt  39947  fprodcncf  40114  dvnmptdivc  40153  dvnprodlem2  40162  dvnprodlem3  40163  stoweidlem6  40223  stoweidlem8  40225  stoweidlem26  40243  stoweidlem31  40248  stoweidlem62  40279  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  sge0iunmpt  40635  ovnsubaddlem1  40784  pfxsuff1eqwrdeq  41407  isgbe  41639  9gbo  41662  11gbo  41663  sbgoldbst  41666  sbgoldbaltlem1  41667  sbgoldbaltlem2  41668  bgoldbtbndlem4  41696  bgoldbtbnd  41697