Theorem 3anbi3d 1445

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  vtocl3gafOLD  3525  vtocl3gaOLD  3527  mob  3663  offval22  8038  smogt  8307  ttrcleq  9630  cfsmolem  10192  fseq1m1p1  13553  pfxsuff1eqwrdeq  14661  2swrd2eqwrdeq  14915  wrdl3s3  14924  prodmo  15901  fprod  15906  divalg  16372  funcres2b  17864  posi  18283  mhmlem  19038  isdrngrd  20743  isdrngrdOLD  20745  lmodlema  20860  connsub  23386  lmmbr3  25227  lmmcvg  25228  dvmptfsum  25942  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupno  27667  nosupfv  27670  noinfcbv  27681  noinfno  27682  noinffv  27685  bdayfinbndlem2  28460  axtg5seg  28533  axtgupdim2  28539  axtgeucl  28540  ishlg  28670  hlcomb  28671  brbtwn  28968  axlowdim  29030  axeuclidlem  29031  usgr2wlkspth  29827  usgr2pth0  29833  wwlksnwwlksnon  29983  usgrwwlks2on  30026  umgrwwlks2on  30027  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  nvi  30685  isslmd  33263  slmdlema  33264  opprlidlabs  33545  constrcccllem  33898  constrcbvlem  33899  inelsros  34322  diffiunisros  34323  hgt749d  34793  tgoldbachgt  34807  axtgupdim2ALTV  34812  afsval  34815  brafs  34816  bnj981  35092  bnj1326  35168  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3  35510  brofs  36187  brifs  36225  cgr3permute1  36230  brcolinear2  36240  colineardim1  36243  brfs  36261  btwnconn1  36283  brsegle  36290  unblimceq0  36767  unbdqndv2  36771  rdgeqoa  37686  iscringd  38319  oposlem  39628  ishlat1  39798  3dim1lem5  39912  lvoli2  40027  cdlemk42  41387  diclspsn  41640  monotoddzz  43371  jm2.27  43436  mendlmod  43617  fiiuncl  45496  wessf1ornlem  45615  infleinf  45801  fmulcl  46011  fmuldfeqlem1  46012  fmuldfeq  46013  climinf2mpt  46142  climinfmpt  46143  fprodcncf  46328  dvnmptdivc  46366  dvnprodlem2  46375  dvnprodlem3  46376  stoweidlem6  46434  stoweidlem8  46436  stoweidlem26  46454  stoweidlem31  46459  stoweidlem62  46490  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  sge0iunmpt  46846  ovnsubaddlem1  46998  isgbe  48227  9gbo  48250  11gbo  48251  sbgoldbst  48254  sbgoldbaltlem1  48255  sbgoldbaltlem2  48256  bgoldbtbndlem4  48284  bgoldbtbnd  48285