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  3516  ceqsex4v  3517  ceqsex8v  3519  vtocl3gafOLD  3561  vtocl3gaOLD  3563  mob  3700  offval22  8087  smogt  8381  ttrcleq  9723  cfsmolem  10284  fseq1m1p1  13616  pfxsuff1eqwrdeq  14717  2swrd2eqwrdeq  14972  wrdl3s3  14981  prodmo  15952  fprod  15957  divalg  16422  funcres2b  17910  posi  18329  mhmlem  19045  isdrngrd  20726  isdrngrdOLD  20728  lmodlema  20822  connsub  23359  lmmbr3  25212  lmmcvg  25213  dvmptfsum  25931  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupno  27667  nosupfv  27670  noinfcbv  27681  noinfno  27682  noinffv  27685  axtg5seg  28444  axtgupdim2  28450  axtgeucl  28451  ishlg  28581  hlcomb  28582  brbtwn  28878  axlowdim  28940  axeuclidlem  28941  usgr2wlkspth  29741  usgr2pth0  29747  wwlksnwwlksnon  29897  umgrwwlks2on  29939  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  nvi  30595  isslmd  33199  slmdlema  33200  opprlidlabs  33500  constrcccllem  33788  constrcbvlem  33789  inelsros  34209  diffiunisros  34210  hgt749d  34681  tgoldbachgt  34695  axtgupdim2ALTV  34700  afsval  34703  brafs  34704  bnj981  34981  bnj1326  35057  cvmlift3lem2  35342  cvmlift3lem4  35344  cvmlift3  35350  brofs  36023  brifs  36061  cgr3permute1  36066  brcolinear2  36076  colineardim1  36079  brfs  36097  btwnconn1  36119  brsegle  36126  unblimceq0  36525  unbdqndv2  36529  rdgeqoa  37388  iscringd  38022  oposlem  39200  ishlat1  39370  3dim1lem5  39485  lvoli2  39600  cdlemk42  40960  diclspsn  41213  monotoddzz  42967  jm2.27  43032  mendlmod  43213  fiiuncl  45089  wessf1ornlem  45209  infleinf  45399  fmulcl  45610  fmuldfeqlem1  45611  fmuldfeq  45612  climinf2mpt  45743  climinfmpt  45744  fprodcncf  45929  dvnmptdivc  45967  dvnprodlem2  45976  dvnprodlem3  45977  stoweidlem6  46035  stoweidlem8  46037  stoweidlem26  46055  stoweidlem31  46060  stoweidlem62  46091  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  sge0iunmpt  46447  ovnsubaddlem1  46599  isgbe  47765  9gbo  47788  11gbo  47789  sbgoldbst  47792  sbgoldbaltlem1  47793  sbgoldbaltlem2  47794  bgoldbtbndlem4  47822  bgoldbtbnd  47823