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  3500  ceqsex4v  3501  ceqsex8v  3503  vtocl3gafOLD  3545  vtocl3gaOLD  3547  mob  3685  offval22  8044  smogt  8313  ttrcleq  9638  cfsmolem  10199  fseq1m1p1  13536  pfxsuff1eqwrdeq  14640  2swrd2eqwrdeq  14895  wrdl3s3  14904  prodmo  15878  fprod  15883  divalg  16349  funcres2b  17835  posi  18254  mhmlem  18970  isdrngrd  20651  isdrngrdOLD  20653  lmodlema  20747  connsub  23284  lmmbr3  25136  lmmcvg  25137  dvmptfsum  25855  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupno  27591  nosupfv  27594  noinfcbv  27605  noinfno  27606  noinffv  27609  axtg5seg  28368  axtgupdim2  28374  axtgeucl  28375  ishlg  28505  hlcomb  28506  brbtwn  28802  axlowdim  28864  axeuclidlem  28865  usgr2wlkspth  29662  usgr2pth0  29668  wwlksnwwlksnon  29818  umgrwwlks2on  29860  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  nvi  30516  isslmd  33128  slmdlema  33129  opprlidlabs  33429  constrcccllem  33717  constrcbvlem  33718  inelsros  34141  diffiunisros  34142  hgt749d  34613  tgoldbachgt  34627  axtgupdim2ALTV  34632  afsval  34635  brafs  34636  bnj981  34913  bnj1326  34989  cvmlift3lem2  35280  cvmlift3lem4  35282  cvmlift3  35288  brofs  35966  brifs  36004  cgr3permute1  36009  brcolinear2  36019  colineardim1  36022  brfs  36040  btwnconn1  36062  brsegle  36069  unblimceq0  36468  unbdqndv2  36472  rdgeqoa  37331  iscringd  37965  oposlem  39148  ishlat1  39318  3dim1lem5  39433  lvoli2  39548  cdlemk42  40908  diclspsn  41161  monotoddzz  42905  jm2.27  42970  mendlmod  43151  fiiuncl  45032  wessf1ornlem  45152  infleinf  45341  fmulcl  45552  fmuldfeqlem1  45553  fmuldfeq  45554  climinf2mpt  45685  climinfmpt  45686  fprodcncf  45871  dvnmptdivc  45909  dvnprodlem2  45918  dvnprodlem3  45919  stoweidlem6  45977  stoweidlem8  45979  stoweidlem26  45997  stoweidlem31  46002  stoweidlem62  46033  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  sge0iunmpt  46389  ovnsubaddlem1  46541  isgbe  47725  9gbo  47748  11gbo  47749  sbgoldbst  47752  sbgoldbaltlem1  47753  sbgoldbaltlem2  47754  bgoldbtbndlem4  47782  bgoldbtbnd  47783