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  3491  ceqsex4v  3492  ceqsex8v  3494  vtocl3gafOLD  3533  vtocl3gaOLD  3535  mob  3671  offval22  8018  smogt  8287  ttrcleq  9599  cfsmolem  10161  fseq1m1p1  13499  pfxsuff1eqwrdeq  14606  2swrd2eqwrdeq  14860  wrdl3s3  14869  prodmo  15843  fprod  15848  divalg  16314  funcres2b  17804  posi  18223  mhmlem  18975  isdrngrd  20681  isdrngrdOLD  20683  lmodlema  20798  connsub  23336  lmmbr3  25187  lmmcvg  25188  dvmptfsum  25906  nosupprefixmo  27639  noinfprefixmo  27640  nosupcbv  27641  nosupno  27642  nosupfv  27645  noinfcbv  27656  noinfno  27657  noinffv  27660  axtg5seg  28443  axtgupdim2  28449  axtgeucl  28450  ishlg  28580  hlcomb  28581  brbtwn  28877  axlowdim  28939  axeuclidlem  28940  usgr2wlkspth  29737  usgr2pth0  29743  wwlksnwwlksnon  29893  usgrwwlks2on  29936  umgrwwlks2on  29937  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  nvi  30594  isslmd  33171  slmdlema  33172  opprlidlabs  33450  constrcccllem  33767  constrcbvlem  33768  inelsros  34191  diffiunisros  34192  hgt749d  34662  tgoldbachgt  34676  axtgupdim2ALTV  34681  afsval  34684  brafs  34685  bnj981  34962  bnj1326  35038  cvmlift3lem2  35364  cvmlift3lem4  35366  cvmlift3  35372  brofs  36049  brifs  36087  cgr3permute1  36092  brcolinear2  36102  colineardim1  36105  brfs  36123  btwnconn1  36145  brsegle  36152  unblimceq0  36551  unbdqndv2  36555  rdgeqoa  37414  iscringd  38037  oposlem  39280  ishlat1  39450  3dim1lem5  39564  lvoli2  39679  cdlemk42  41039  diclspsn  41292  monotoddzz  43035  jm2.27  43100  mendlmod  43281  fiiuncl  45161  wessf1ornlem  45281  infleinf  45469  fmulcl  45680  fmuldfeqlem1  45681  fmuldfeq  45682  climinf2mpt  45811  climinfmpt  45812  fprodcncf  45997  dvnmptdivc  46035  dvnprodlem2  46044  dvnprodlem3  46045  stoweidlem6  46103  stoweidlem8  46105  stoweidlem26  46123  stoweidlem31  46128  stoweidlem62  46159  fourierdlem41  46245  fourierdlem48  46251  fourierdlem49  46252  sge0iunmpt  46515  ovnsubaddlem1  46667  isgbe  47850  9gbo  47873  11gbo  47874  sbgoldbst  47877  sbgoldbaltlem1  47878  sbgoldbaltlem2  47879  bgoldbtbndlem4  47907  bgoldbtbnd  47908