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  3505  ceqsex4v  3506  ceqsex8v  3508  mob  3678  offval22  8089  smogt  8360  ttrcleq  9692  cfsmolem  10276  fseq1m1p1  13658  pfxsuff1eqwrdeq  14772  2swrd2eqwrdeq  15030  wrdl3s3  15039  prodmo  16029  fprod  16034  divalg  16499  funcres2b  17992  posi  18411  mhmlem  19191  isdrngrd  20938  isdrngrdOLD  20940  lmodlema  21055  connsub  23652  lmmbr3  25494  lmmcvg  25495  dvmptfsum  26209  nosupprefixmo  27944  noinfprefixmo  27945  nosupcbv  27946  nosupno  27947  nosupfv  27950  noinfcbv  27961  noinfno  27962  noinffv  27965  bdayfinbndlem2  28741  axtg5seg  28814  axtgupdim2  28820  axtgeucl  28821  ishlg2  28952  ishlg  28955  hlcomb  28956  brbtwn  29364  axlowdim  29426  axeuclidlem  29427  usgr2wlkspth  30232  usgr2pth0  30238  wwlksnwwlksnon  30391  usgrwwlks2on  30434  umgrwwlks2on  30435  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  nvi  31103  isslmd  33650  slmdlema  33651  opprlidlabs  33895  constrcccllem  34272  constrcbvlem  34273  inelsros  34697  diffiunisros  34698  hgt749d  35165  tgoldbachgt  35179  axtgupdim2ALTV  35184  afsval  35190  brafs  35191  bnj981  35467  bnj1326  35543  cvmlift3lem2  35907  cvmlift3lem4  35909  cvmlift3  35915  brofs  36593  brifs  36631  cgr3permute1  36636  brcolinear2  36646  colineardim1  36649  brfs  36667  btwnconn1  36689  brsegle  36696  unblimceq0  37212  unbdqndv2  37216  rdgeqoa  38132  iscringd  38756  oposlem  40063  ishlat1  40233  3dim1lem5  40347  lvoli2  40462  cdlemk42  41822  diclspsn  42075  monotoddzz  43792  jm2.27  43857  mendlmod  44038  fiiuncl  45907  wessf1ornlem  46025  infleinf  46209  fmulcl  46419  fmuldfeqlem1  46420  fmuldfeq  46421  climinf2mpt  46550  climinfmpt  46551  fprodcncf  46736  dvnmptdivc  46774  dvnprodlem2  46783  dvnprodlem3  46784  stoweidlem6  46842  stoweidlem8  46844  stoweidlem26  46862  stoweidlem31  46867  stoweidlem62  46898  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  sge0iunmpt  47254  ovnsubaddlem1  47406  isgbe  48675  9gbo  48698  11gbo  48699  sbgoldbst  48702  sbgoldbaltlem1  48703  sbgoldbaltlem2  48704  bgoldbtbndlem4  48732  bgoldbtbnd  48733