Theorem 3anbi3d 1444

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  vtocl3gafOLD  3551  vtocl3gaOLD  3553  mob  3691  offval22  8070  smogt  8339  ttrcleq  9669  cfsmolem  10230  fseq1m1p1  13567  pfxsuff1eqwrdeq  14671  2swrd2eqwrdeq  14926  wrdl3s3  14935  prodmo  15909  fprod  15914  divalg  16380  funcres2b  17866  posi  18285  mhmlem  19001  isdrngrd  20682  isdrngrdOLD  20684  lmodlema  20778  connsub  23315  lmmbr3  25167  lmmcvg  25168  dvmptfsum  25886  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupno  27622  nosupfv  27625  noinfcbv  27636  noinfno  27637  noinffv  27640  axtg5seg  28399  axtgupdim2  28405  axtgeucl  28406  ishlg  28536  hlcomb  28537  brbtwn  28833  axlowdim  28895  axeuclidlem  28896  usgr2wlkspth  29696  usgr2pth0  29702  wwlksnwwlksnon  29852  umgrwwlks2on  29894  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  nvi  30550  isslmd  33162  slmdlema  33163  opprlidlabs  33463  constrcccllem  33751  constrcbvlem  33752  inelsros  34175  diffiunisros  34176  hgt749d  34647  tgoldbachgt  34661  axtgupdim2ALTV  34666  afsval  34669  brafs  34670  bnj981  34947  bnj1326  35023  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3  35322  brofs  36000  brifs  36038  cgr3permute1  36043  brcolinear2  36053  colineardim1  36056  brfs  36074  btwnconn1  36096  brsegle  36103  unblimceq0  36502  unbdqndv2  36506  rdgeqoa  37365  iscringd  37999  oposlem  39182  ishlat1  39352  3dim1lem5  39467  lvoli2  39582  cdlemk42  40942  diclspsn  41195  monotoddzz  42939  jm2.27  43004  mendlmod  43185  fiiuncl  45066  wessf1ornlem  45186  infleinf  45375  fmulcl  45586  fmuldfeqlem1  45587  fmuldfeq  45588  climinf2mpt  45719  climinfmpt  45720  fprodcncf  45905  dvnmptdivc  45943  dvnprodlem2  45952  dvnprodlem3  45953  stoweidlem6  46011  stoweidlem8  46013  stoweidlem26  46031  stoweidlem31  46036  stoweidlem62  46067  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  sge0iunmpt  46423  ovnsubaddlem1  46575  isgbe  47756  9gbo  47779  11gbo  47780  sbgoldbst  47783  sbgoldbaltlem1  47784  sbgoldbaltlem2  47785  bgoldbtbndlem4  47813  bgoldbtbnd  47814