Theorem 3anbi3d 1470

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 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1466	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  mob  3675  offval22  8085  smogt  8356  ttrcleq  9688  cfsmolem  10272  fseq1m1p1  13654  pfxsuff1eqwrdeq  14768  2swrd2eqwrdeq  15026  wrdl3s3  15035  prodmo  16023  fprod  16028  divalg  16493  funcres2b  17986  posi  18405  mhmlem  19185  isdrngrd  20932  isdrngrdOLD  20934  lmodlema  21049  connsub  23646  lmmbr3  25488  lmmcvg  25489  dvmptfsum  26202  nosupprefixmo  27936  noinfprefixmo  27937  nosupcbv  27938  nosupno  27939  nosupfv  27942  noinfcbv  27953  noinfno  27954  noinffv  27957  bdayfinbndlem2  28733  axtg5seg  28806  axtgupdim2  28812  axtgeucl  28813  ishlg2  28944  ishlg  28947  hlcomb  28948  brbtwn  29356  axlowdim  29418  axeuclidlem  29419  usgr2wlkspth  30224  usgr2pth0  30230  wwlksnwwlksnon  30383  usgrwwlks2on  30426  umgrwwlks2on  30427  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  nvi  31095  isslmd  33642  slmdlema  33643  opprlidlabs  33887  constrcccllem  34264  constrcbvlem  34265  inelsros  34689  diffiunisros  34690  hgt749d  35157  tgoldbachgt  35171  axtgupdim2ALTV  35176  afsval  35182  brafs  35183  bnj981  35459  bnj1326  35535  cvmlift3lem2  35899  cvmlift3lem4  35901  cvmlift3  35907  brofs  36585  brifs  36623  cgr3permute1  36628  brcolinear2  36638  colineardim1  36641  brfs  36659  btwnconn1  36681  brsegle  36688  unblimceq0  37204  unbdqndv2  37208  rdgeqoa  38124  iscringd  38748  oposlem  40055  ishlat1  40225  3dim1lem5  40339  lvoli2  40454  cdlemk42  41814  diclspsn  42067  monotoddzz  43784  jm2.27  43849  mendlmod  44030  fiiuncl  45899  wessf1ornlem  46017  infleinf  46201  fmulcl  46411  fmuldfeqlem1  46412  fmuldfeq  46413  climinf2mpt  46542  climinfmpt  46543  fprodcncf  46728  dvnmptdivc  46766  dvnprodlem2  46775  dvnprodlem3  46776  stoweidlem6  46834  stoweidlem8  46836  stoweidlem26  46854  stoweidlem31  46859  stoweidlem62  46890  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  sge0iunmpt  47246  ovnsubaddlem1  47398  isgbe  48667  9gbo  48690  11gbo  48691  sbgoldbst  48694  sbgoldbaltlem1  48695  sbgoldbaltlem2  48696  bgoldbtbndlem4  48724  bgoldbtbnd  48725