Theorem 3anbi3d 1441

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ceqsex3v  3485  ceqsex4v  3486  ceqsex8v  3488  vtocl3gaf  3517  vtocl3ga  3518  mob  3653  dfopif  4801  offval22  7937  smogt  8207  ttrcleq  9476  cfsmolem  10035  fseq1m1p1  13340  pfxsuff1eqwrdeq  14421  2swrd2eqwrdeq  14675  wrdl3s3  14686  prodmo  15655  fprod  15660  divalg  16121  funcres2b  17621  posi  18044  mhmlem  18704  isdrngrd  20026  lmodlema  20137  connsub  22581  lmmbr3  24433  lmmcvg  24434  dvmptfsum  25148  axtg5seg  26835  axtgupdim2  26841  axtgeucl  26842  ishlg  26972  hlcomb  26973  brbtwn  27276  axlowdim  27338  axeuclidlem  27339  usgr2wlkspth  28136  usgr2pth0  28142  wwlksnwwlksnon  28289  umgrwwlks2on  28331  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  nvi  28985  isslmd  31464  slmdlema  31465  inelsros  32155  diffiunisros  32156  hgt749d  32638  tgoldbachgt  32652  axtgupdim2ALTV  32657  afsval  32660  brafs  32661  bnj981  32939  bnj1326  33015  cvmlift3lem2  33291  cvmlift3lem4  33293  cvmlift3  33299  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupno  33915  nosupfv  33918  noinfcbv  33929  noinfno  33930  noinffv  33933  brofs  34316  brifs  34354  cgr3permute1  34359  brcolinear2  34369  colineardim1  34372  brfs  34390  btwnconn1  34412  brsegle  34419  unblimceq0  34696  unbdqndv2  34700  rdgeqoa  35550  iscringd  36165  oposlem  37203  ishlat1  37373  3dim1lem5  37487  lvoli2  37602  cdlemk42  38962  diclspsn  39215  monotoddzz  40772  jm2.27  40837  mendlmod  41025  fiiuncl  42620  wessf1ornlem  42729  infleinf  42918  fmulcl  43129  fmuldfeqlem1  43130  fmuldfeq  43131  climinf2mpt  43262  climinfmpt  43263  fprodcncf  43448  dvnmptdivc  43486  dvnprodlem2  43495  dvnprodlem3  43496  stoweidlem6  43554  stoweidlem8  43556  stoweidlem26  43574  stoweidlem31  43579  stoweidlem62  43610  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  sge0iunmpt  43963  ovnsubaddlem1  44115  isgbe  45214  9gbo  45237  11gbo  45238  sbgoldbst  45241  sbgoldbaltlem1  45242  sbgoldbaltlem2  45243  bgoldbtbndlem4  45271  bgoldbtbnd  45272