Theorem 3anbi3d 1397

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 251	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1393	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  vtocl3gaf  3248  mob  3355  offval22  7140  smogt  7351  cfsmolem  8975  fseq1m1p1  12284  2swrd1eqwrdeq  13306  2swrd2eqwrdeq  13544  wrdl3s3  13553  prodmo  14505  fprod  14510  divalg  14964  funcres2b  16380  posi  16773  mhmlem  17358  isdrngrd  18596  lmodlema  18691  connsub  21034  lmmbr3  22866  lmmcvg  22867  dvmptfsum  23542  axtg5seg  25164  axtgupdim2  25170  axtgeucl  25171  ishlg  25297  hlcomb  25298  brbtwn  25579  axlowdim  25641  axeuclidlem  25642  1pthoncl  26122  3v3e3cycl1  26172  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  usg2wlkonot  26410  rusgra0edg  26482  2spotdisj  26588  nvi  26853  isslmd  29086  slmdlema  29087  inelsros  29568  diffiunisros  29569  axtgupdim2OLD  29999  afsval  30002  brafs  30003  bnj981  30274  bnj1326  30348  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3  30564  frrlem1  31024  brofs  31282  brifs  31320  cgr3permute1  31325  brcolinear2  31335  colineardim1  31338  brfs  31356  btwnconn1  31378  brsegle  31385  unblimceq0  31668  unbdqndv2  31672  rdgeqoa  32394  iscringd  32967  oposlem  33487  ishlat1  33657  3dim1lem5  33770  lvoli2  33885  cdlemk42  35247  diclspsn  35501  monotoddzz  36526  jm2.27  36593  mendlmod  36782  fiiuncl  38259  wessf1ornlem  38366  infleinf  38529  fmulcl  38648  fmuldfeqlem1  38649  fmuldfeq  38650  fprodcncf  38787  dvnmptdivc  38828  dvnprodlem2  38837  dvnprodlem3  38838  stoweidlem6  38899  stoweidlem8  38901  stoweidlem26  38919  stoweidlem31  38924  stoweidlem62  38955  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  sge0iunmpt  39311  ovnsubaddlem1  39460  isgbe  40173  9gboa  40196  11gboa  40197  bgoldbst  40200  sgoldbaltlem1  40201  sgoldbaltlem2  40202  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxsuff1eqwrdeq  40270  usgr2wlkspth  40965  usgr2pth0  40971  wwlksnwwlksnon  41121  umgrwwlks2on  41161  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352