Theorem 3anbi3d 1442

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  vtocl3gafOLD  3594  vtocl3gaOLD  3596  mob  3739  offval22  8129  smogt  8423  ttrcleq  9778  cfsmolem  10339  fseq1m1p1  13659  pfxsuff1eqwrdeq  14747  2swrd2eqwrdeq  15002  wrdl3s3  15011  prodmo  15984  fprod  15989  divalg  16451  funcres2b  17961  posi  18387  mhmlem  19102  isdrngrd  20788  isdrngrdOLD  20790  lmodlema  20885  connsub  23450  lmmbr3  25313  lmmcvg  25314  dvmptfsum  26033  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupno  27766  nosupfv  27769  noinfcbv  27780  noinfno  27781  noinffv  27784  axtg5seg  28491  axtgupdim2  28497  axtgeucl  28498  ishlg  28628  hlcomb  28629  brbtwn  28932  axlowdim  28994  axeuclidlem  28995  usgr2wlkspth  29795  usgr2pth0  29801  wwlksnwwlksnon  29948  umgrwwlks2on  29990  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  nvi  30646  isslmd  33181  slmdlema  33182  opprlidlabs  33478  inelsros  34142  diffiunisros  34143  hgt749d  34626  tgoldbachgt  34640  axtgupdim2ALTV  34645  afsval  34648  brafs  34649  bnj981  34926  bnj1326  35002  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3  35296  brofs  35969  brifs  36007  cgr3permute1  36012  brcolinear2  36022  colineardim1  36025  brfs  36043  btwnconn1  36065  brsegle  36072  unblimceq0  36473  unbdqndv2  36477  rdgeqoa  37336  iscringd  37958  oposlem  39138  ishlat1  39308  3dim1lem5  39423  lvoli2  39538  cdlemk42  40898  diclspsn  41151  monotoddzz  42900  jm2.27  42965  mendlmod  43150  fiiuncl  44967  wessf1ornlem  45092  infleinf  45287  fmulcl  45502  fmuldfeqlem1  45503  fmuldfeq  45504  climinf2mpt  45635  climinfmpt  45636  fprodcncf  45821  dvnmptdivc  45859  dvnprodlem2  45868  dvnprodlem3  45869  stoweidlem6  45927  stoweidlem8  45929  stoweidlem26  45947  stoweidlem31  45952  stoweidlem62  45983  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  sge0iunmpt  46339  ovnsubaddlem1  46491  isgbe  47625  9gbo  47648  11gbo  47649  sbgoldbst  47652  sbgoldbaltlem1  47653  sbgoldbaltlem2  47654  bgoldbtbndlem4  47682  bgoldbtbnd  47683