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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  mob  3680  offval22  8079  smogt  8350  ttrcleq  9674  cfsmolem  10249  fseq1m1p1  13623  pfxsuff1eqwrdeq  14732  2swrd2eqwrdeq  14986  wrdl3s3  14995  prodmo  15986  fprod  15991  divalg  16456  funcres2b  17949  posi  18368  mhmlem  19123  isdrngrd  20869  isdrngrdOLD  20871  lmodlema  20986  connsub  23578  lmmbr3  25419  lmmcvg  25420  dvmptfsum  26134  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupno  27867  nosupfv  27870  noinfcbv  27881  noinfno  27882  noinffv  27885  bdayfinbndlem2  28661  axtg5seg  28734  axtgupdim2  28740  axtgeucl  28741  ishlg2  28871  ishlg  28874  hlcomb  28875  brbtwn  29249  axlowdim  29311  axeuclidlem  29312  usgr2wlkspth  30108  usgr2pth0  30114  wwlksnwwlksnon  30264  usgrwwlks2on  30307  umgrwwlks2on  30308  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  nvi  30966  isslmd  33522  slmdlema  33523  opprlidlabs  33767  constrcccllem  34144  constrcbvlem  34145  inelsros  34568  diffiunisros  34569  hgt749d  35036  tgoldbachgt  35050  axtgupdim2ALTV  35055  afsval  35061  brafs  35062  bnj981  35338  bnj1326  35414  cvmlift3lem2  35812  cvmlift3lem4  35814  cvmlift3  35820  brofs  36497  brifs  36535  cgr3permute1  36540  brcolinear2  36550  colineardim1  36553  brfs  36571  btwnconn1  36593  brsegle  36600  unblimceq0  37096  unbdqndv2  37100  rdgeqoa  38016  iscringd  38649  oposlem  39956  ishlat1  40126  3dim1lem5  40240  lvoli2  40355  cdlemk42  41715  diclspsn  41968  monotoddzz  43670  jm2.27  43735  mendlmod  43916  fiiuncl  45785  wessf1ornlem  45903  infleinf  46087  fmulcl  46297  fmuldfeqlem1  46298  fmuldfeq  46299  climinf2mpt  46428  climinfmpt  46429  fprodcncf  46614  dvnmptdivc  46652  dvnprodlem2  46661  dvnprodlem3  46662  stoweidlem6  46720  stoweidlem8  46722  stoweidlem26  46740  stoweidlem31  46745  stoweidlem62  46776  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  sge0iunmpt  47132  ovnsubaddlem1  47284  isgbe  48516  9gbo  48539  11gbo  48540  sbgoldbst  48543  sbgoldbaltlem1  48544  sbgoldbaltlem2  48545  bgoldbtbndlem4  48573  bgoldbtbnd  48574