Theorem 3anbi3d 1434

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 1430	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

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

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 1082

This theorem is referenced by:  ceqsex3v  3487  ceqsex4v  3488  ceqsex8v  3490  vtocl3gaf  3518  mob  3645  offval22  7642  smogt  7859  cfsmolem  9541  fseq1m1p1  12832  pfxsuff1eqwrdeq  13897  2swrd2eqwrdeq  14151  wrdl3s3  14160  prodmo  15123  fprod  15128  divalg  15587  funcres2b  16996  posi  17389  mhmlem  17976  isdrngrd  19218  lmodlema  19329  connsub  21713  lmmbr3  23546  lmmcvg  23547  dvmptfsum  24255  axtg5seg  25933  axtgupdim2  25939  axtgeucl  25940  ishlg  26070  hlcomb  26071  brbtwn  26368  axlowdim  26430  axeuclidlem  26431  usgr2wlkspth  27222  usgr2pth0  27228  wwlksnwwlksnon  27376  umgrwwlks2on  27418  upgr3v3e3cycl  27641  upgr4cycl4dv4e  27646  nvi  28074  isslmd  30460  slmdlema  30461  inelsros  31046  diffiunisros  31047  hgt749d  31529  tgoldbachgt  31543  axtgupdim2ALTV  31548  afsval  31551  brafs  31552  bnj981  31830  bnj1326  31904  cvmlift3lem2  32169  cvmlift3lem4  32171  cvmlift3  32177  noprefixmo  32805  nosupno  32806  nosupfv  32809  brofs  33069  brifs  33107  cgr3permute1  33112  brcolinear2  33122  colineardim1  33125  brfs  33143  btwnconn1  33165  brsegle  33172  unblimceq0  33449  unbdqndv2  33453  rdgeqoa  34195  iscringd  34821  oposlem  35862  ishlat1  36032  3dim1lem5  36146  lvoli2  36261  cdlemk42  37621  diclspsn  37874  monotoddzz  39038  jm2.27  39103  mendlmod  39291  fiiuncl  40879  wessf1ornlem  40998  infleinf  41194  fmulcl  41417  fmuldfeqlem1  41418  fmuldfeq  41419  climinf2mpt  41550  climinfmpt  41551  fprodcncf  41739  dvnmptdivc  41778  dvnprodlem2  41787  dvnprodlem3  41788  stoweidlem6  41847  stoweidlem8  41849  stoweidlem26  41867  stoweidlem31  41872  stoweidlem62  41903  fourierdlem41  41989  fourierdlem48  41995  fourierdlem49  41996  sge0iunmpt  42256  ovnsubaddlem1  42408  isgbe  43412  9gbo  43435  11gbo  43436  sbgoldbst  43439  sbgoldbaltlem1  43440  sbgoldbaltlem2  43441  bgoldbtbndlem4  43469  bgoldbtbnd  43470