Theorem 3anbi3d 1441

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 1437	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  3536  ceqsex4v  3537  ceqsex8v  3539  vtocl3gafOLD  3581  vtocl3gaOLD  3583  mob  3725  offval22  8111  smogt  8405  ttrcleq  9746  cfsmolem  10307  fseq1m1p1  13635  pfxsuff1eqwrdeq  14733  2swrd2eqwrdeq  14988  wrdl3s3  14997  prodmo  15968  fprod  15973  divalg  16436  funcres2b  17947  posi  18374  mhmlem  19092  isdrngrd  20782  isdrngrdOLD  20784  lmodlema  20879  connsub  23444  lmmbr3  25307  lmmcvg  25308  dvmptfsum  26027  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupno  27762  nosupfv  27765  noinfcbv  27776  noinfno  27777  noinffv  27780  axtg5seg  28487  axtgupdim2  28493  axtgeucl  28494  ishlg  28624  hlcomb  28625  brbtwn  28928  axlowdim  28990  axeuclidlem  28991  usgr2wlkspth  29791  usgr2pth0  29797  wwlksnwwlksnon  29944  umgrwwlks2on  29986  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  nvi  30642  isslmd  33190  slmdlema  33191  opprlidlabs  33492  inelsros  34158  diffiunisros  34159  hgt749d  34642  tgoldbachgt  34656  axtgupdim2ALTV  34661  afsval  34664  brafs  34665  bnj981  34942  bnj1326  35018  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3  35312  brofs  35986  brifs  36024  cgr3permute1  36029  brcolinear2  36039  colineardim1  36042  brfs  36060  btwnconn1  36082  brsegle  36089  unblimceq0  36489  unbdqndv2  36493  rdgeqoa  37352  iscringd  37984  oposlem  39163  ishlat1  39333  3dim1lem5  39448  lvoli2  39563  cdlemk42  40923  diclspsn  41176  monotoddzz  42931  jm2.27  42996  mendlmod  43177  fiiuncl  45004  wessf1ornlem  45127  infleinf  45321  fmulcl  45536  fmuldfeqlem1  45537  fmuldfeq  45538  climinf2mpt  45669  climinfmpt  45670  fprodcncf  45855  dvnmptdivc  45893  dvnprodlem2  45902  dvnprodlem3  45903  stoweidlem6  45961  stoweidlem8  45963  stoweidlem26  45981  stoweidlem31  45986  stoweidlem62  46017  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  sge0iunmpt  46373  ovnsubaddlem1  46525  isgbe  47675  9gbo  47698  11gbo  47699  sbgoldbst  47702  sbgoldbaltlem1  47703  sbgoldbaltlem2  47704  bgoldbtbndlem4  47732  bgoldbtbnd  47733