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  36047  brifs  36085  cgr3permute1  36090  brcolinear2  36100  colineardim1  36103  brfs  36121  btwnconn1  36143  brsegle  36150  unblimceq0  36549  unbdqndv2  36553  rdgeqoa  37412  iscringd  38046  oposlem  39229  ishlat1  39399  3dim1lem5  39513  lvoli2  39628  cdlemk42  40988  diclspsn  41241  monotoddzz  42984  jm2.27  43049  mendlmod  43230  fiiuncl  45110  wessf1ornlem  45230  infleinf  45418  fmulcl  45629  fmuldfeqlem1  45630  fmuldfeq  45631  climinf2mpt  45760  climinfmpt  45761  fprodcncf  45946  dvnmptdivc  45984  dvnprodlem2  45993  dvnprodlem3  45994  stoweidlem6  46052  stoweidlem8  46054  stoweidlem26  46072  stoweidlem31  46077  stoweidlem62  46108  fourierdlem41  46194  fourierdlem48  46200  fourierdlem49  46201  sge0iunmpt  46464  ovnsubaddlem1  46616  isgbe  47790  9gbo  47813  11gbo  47814  sbgoldbst  47817  sbgoldbaltlem1  47818  sbgoldbaltlem2  47819  bgoldbtbndlem4  47847  bgoldbtbnd  47848