Theorem 3anbi3d 1438

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

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi3d	⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		biidd 264	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1434	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  vtocl3gaf  3564  mob  3694  offval22  7764  smogt  7985  cfsmolem  9673  fseq1m1p1  12967  pfxsuff1eqwrdeq  14041  2swrd2eqwrdeq  14295  wrdl3s3  14306  prodmo  15270  fprod  15275  divalg  15732  funcres2b  17145  posi  17538  mhmlem  18197  isdrngrd  19506  lmodlema  19617  connsub  22007  lmmbr3  23841  lmmcvg  23842  dvmptfsum  24552  axtg5seg  26232  axtgupdim2  26238  axtgeucl  26239  ishlg  26369  hlcomb  26370  brbtwn  26666  axlowdim  26728  axeuclidlem  26729  usgr2wlkspth  27521  usgr2pth0  27527  wwlksnwwlksnon  27674  umgrwwlks2on  27716  upgr3v3e3cycl  27938  upgr4cycl4dv4e  27943  nvi  28370  isslmd  30832  slmdlema  30833  inelsros  31439  diffiunisros  31440  hgt749d  31922  tgoldbachgt  31936  axtgupdim2ALTV  31941  afsval  31944  brafs  31945  bnj981  32224  bnj1326  32300  cvmlift3lem2  32569  cvmlift3lem4  32571  cvmlift3  32577  noprefixmo  33204  nosupno  33205  nosupfv  33208  brofs  33468  brifs  33506  cgr3permute1  33511  brcolinear2  33521  colineardim1  33524  brfs  33542  btwnconn1  33564  brsegle  33571  unblimceq0  33848  unbdqndv2  33852  rdgeqoa  34662  iscringd  35303  oposlem  36345  ishlat1  36515  3dim1lem5  36629  lvoli2  36744  cdlemk42  38104  diclspsn  38357  monotoddzz  39627  jm2.27  39692  mendlmod  39880  fiiuncl  41412  wessf1ornlem  41530  infleinf  41725  fmulcl  41947  fmuldfeqlem1  41948  fmuldfeq  41949  climinf2mpt  42080  climinfmpt  42081  fprodcncf  42269  dvnmptdivc  42308  dvnprodlem2  42317  dvnprodlem3  42318  stoweidlem6  42376  stoweidlem8  42378  stoweidlem26  42396  stoweidlem31  42401  stoweidlem62  42432  fourierdlem41  42518  fourierdlem48  42524  fourierdlem49  42525  sge0iunmpt  42785  ovnsubaddlem1  42937  isgbe  43996  9gbo  44019  11gbo  44020  sbgoldbst  44023  sbgoldbaltlem1  44024  sbgoldbaltlem2  44025  bgoldbtbndlem4  44053  bgoldbtbnd  44054