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 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  3537  ceqsex4v  3538  ceqsex8v  3540  vtocl3gafOLD  3582  vtocl3gaOLD  3584  mob  3723  offval22  8113  smogt  8407  ttrcleq  9749  cfsmolem  10310  fseq1m1p1  13639  pfxsuff1eqwrdeq  14737  2swrd2eqwrdeq  14992  wrdl3s3  15001  prodmo  15972  fprod  15977  divalg  16440  funcres2b  17942  posi  18363  mhmlem  19080  isdrngrd  20766  isdrngrdOLD  20768  lmodlema  20863  connsub  23429  lmmbr3  25294  lmmcvg  25295  dvmptfsum  26013  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupno  27748  nosupfv  27751  noinfcbv  27762  noinfno  27763  noinffv  27766  axtg5seg  28473  axtgupdim2  28479  axtgeucl  28480  ishlg  28610  hlcomb  28611  brbtwn  28914  axlowdim  28976  axeuclidlem  28977  usgr2wlkspth  29779  usgr2pth0  29785  wwlksnwwlksnon  29935  umgrwwlks2on  29977  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  nvi  30633  isslmd  33208  slmdlema  33209  opprlidlabs  33513  inelsros  34179  diffiunisros  34180  hgt749d  34664  tgoldbachgt  34678  axtgupdim2ALTV  34683  afsval  34686  brafs  34687  bnj981  34964  bnj1326  35040  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3  35333  brofs  36006  brifs  36044  cgr3permute1  36049  brcolinear2  36059  colineardim1  36062  brfs  36080  btwnconn1  36102  brsegle  36109  unblimceq0  36508  unbdqndv2  36512  rdgeqoa  37371  iscringd  38005  oposlem  39183  ishlat1  39353  3dim1lem5  39468  lvoli2  39583  cdlemk42  40943  diclspsn  41196  monotoddzz  42955  jm2.27  43020  mendlmod  43201  fiiuncl  45070  wessf1ornlem  45190  infleinf  45383  fmulcl  45596  fmuldfeqlem1  45597  fmuldfeq  45598  climinf2mpt  45729  climinfmpt  45730  fprodcncf  45915  dvnmptdivc  45953  dvnprodlem2  45962  dvnprodlem3  45963  stoweidlem6  46021  stoweidlem8  46023  stoweidlem26  46041  stoweidlem31  46046  stoweidlem62  46077  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  sge0iunmpt  46433  ovnsubaddlem1  46585  isgbe  47738  9gbo  47761  11gbo  47762  sbgoldbst  47765  sbgoldbaltlem1  47766  sbgoldbaltlem2  47767  bgoldbtbndlem4  47795  bgoldbtbnd  47796