Theorem 3anbi3d 1450

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  mob  3658  offval22  8027  smogt  8297  ttrcleq  9621  cfsmolem  10183  fseq1m1p1  13544  pfxsuff1eqwrdeq  14652  2swrd2eqwrdeq  14906  wrdl3s3  14915  prodmo  15892  fprod  15897  divalg  16363  funcres2b  17855  posi  18274  mhmlem  19029  isdrngrd  20738  isdrngrdOLD  20740  lmodlema  20855  connsub  23404  lmmbr3  25245  lmmcvg  25246  dvmptfsum  25960  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupno  27685  nosupfv  27688  noinfcbv  27699  noinfno  27700  noinffv  27703  bdayfinbndlem2  28478  axtg5seg  28551  axtgupdim2  28557  axtgeucl  28558  ishlg  28688  hlcomb  28689  brbtwn  28986  axlowdim  29048  axeuclidlem  29049  usgr2wlkspth  29845  usgr2pth0  29851  wwlksnwwlksnon  30001  usgrwwlks2on  30044  umgrwwlks2on  30045  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  nvi  30703  isslmd  33283  slmdlema  33284  opprlidlabs  33568  constrcccllem  33938  constrcbvlem  33939  inelsros  34362  diffiunisros  34363  hgt749d  34833  tgoldbachgt  34847  axtgupdim2ALTV  34852  afsval  34855  brafs  34856  bnj981  35132  bnj1326  35208  cvmlift3lem2  35548  cvmlift3lem4  35550  cvmlift3  35556  brofs  36233  brifs  36271  cgr3permute1  36276  brcolinear2  36286  colineardim1  36289  brfs  36307  btwnconn1  36329  brsegle  36336  unblimceq0  36813  unbdqndv2  36817  rdgeqoa  37732  iscringd  38365  oposlem  39674  ishlat1  39844  3dim1lem5  39958  lvoli2  40073  cdlemk42  41433  diclspsn  41686  monotoddzz  43388  jm2.27  43453  mendlmod  43634  fiiuncl  45513  wessf1ornlem  45632  infleinf  45816  fmulcl  46026  fmuldfeqlem1  46027  fmuldfeq  46028  climinf2mpt  46157  climinfmpt  46158  fprodcncf  46343  dvnmptdivc  46381  dvnprodlem2  46390  dvnprodlem3  46391  stoweidlem6  46449  stoweidlem8  46451  stoweidlem26  46469  stoweidlem31  46474  stoweidlem62  46505  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  sge0iunmpt  46861  ovnsubaddlem1  47013  isgbe  48242  9gbo  48265  11gbo  48266  sbgoldbst  48269  sbgoldbaltlem1  48270  sbgoldbaltlem2  48271  bgoldbtbndlem4  48299  bgoldbtbnd  48300