Theorem 3anbi3d 1443

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  vtocl3gaf  3569  vtocl3ga  3570  mob  3714  offval22  8074  smogt  8367  ttrcleq  9704  cfsmolem  10265  fseq1m1p1  13576  pfxsuff1eqwrdeq  14649  2swrd2eqwrdeq  14904  wrdl3s3  14913  prodmo  15880  fprod  15885  divalg  16346  funcres2b  17847  posi  18270  mhmlem  18945  isdrngrd  20391  isdrngrdOLD  20393  lmodlema  20476  connsub  22925  lmmbr3  24777  lmmcvg  24778  dvmptfsum  25492  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupno  27206  nosupfv  27209  noinfcbv  27220  noinfno  27221  noinffv  27224  axtg5seg  27716  axtgupdim2  27722  axtgeucl  27723  ishlg  27853  hlcomb  27854  brbtwn  28157  axlowdim  28219  axeuclidlem  28220  usgr2wlkspth  29016  usgr2pth0  29022  wwlksnwwlksnon  29169  umgrwwlks2on  29211  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  nvi  29867  isslmd  32347  slmdlema  32348  opprlidlabs  32599  inelsros  33176  diffiunisros  33177  hgt749d  33661  tgoldbachgt  33675  axtgupdim2ALTV  33680  afsval  33683  brafs  33684  bnj981  33961  bnj1326  34037  cvmlift3lem2  34311  cvmlift3lem4  34313  cvmlift3  34319  brofs  34977  brifs  35015  cgr3permute1  35020  brcolinear2  35030  colineardim1  35033  brfs  35051  btwnconn1  35073  brsegle  35080  unblimceq0  35383  unbdqndv2  35387  rdgeqoa  36251  iscringd  36866  oposlem  38052  ishlat1  38222  3dim1lem5  38337  lvoli2  38452  cdlemk42  39812  diclspsn  40065  monotoddzz  41682  jm2.27  41747  mendlmod  41935  fiiuncl  43752  wessf1ornlem  43882  infleinf  44082  fmulcl  44297  fmuldfeqlem1  44298  fmuldfeq  44299  climinf2mpt  44430  climinfmpt  44431  fprodcncf  44616  dvnmptdivc  44654  dvnprodlem2  44663  dvnprodlem3  44664  stoweidlem6  44722  stoweidlem8  44724  stoweidlem26  44742  stoweidlem31  44747  stoweidlem62  44778  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  sge0iunmpt  45134  ovnsubaddlem1  45286  isgbe  46419  9gbo  46442  11gbo  46443  sbgoldbst  46446  sbgoldbaltlem1  46447  sbgoldbaltlem2  46448  bgoldbtbndlem4  46476  bgoldbtbnd  46477