Theorem 3anbi3d 1463

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 264	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1459	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  mob  3680  offval22  8067  smogt  8338  ttrcleq  9664  cfsmolem  10227  fseq1m1p1  13604  pfxsuff1eqwrdeq  14712  2swrd2eqwrdeq  14966  wrdl3s3  14975  prodmo  15966  fprod  15971  divalg  16437  funcres2b  17930  posi  18349  mhmlem  19104  isdrngrd  20812  isdrngrdOLD  20814  lmodlema  20929  connsub  23478  lmmbr3  25319  lmmcvg  25320  dvmptfsum  26034  nosupprefixmo  27761  noinfprefixmo  27762  nosupcbv  27763  nosupno  27764  nosupfv  27767  noinfcbv  27778  noinfno  27779  noinffv  27782  bdayfinbndlem2  28558  axtg5seg  28631  axtgupdim2  28637  axtgeucl  28638  ishlg  28768  hlcomb  28769  brbtwn  29097  axlowdim  29159  axeuclidlem  29160  usgr2wlkspth  29956  usgr2pth0  29962  wwlksnwwlksnon  30112  usgrwwlks2on  30155  umgrwwlks2on  30156  upgr3v3e3cycl  30379  upgr4cycl4dv4e  30384  nvi  30814  isslmd  33379  slmdlema  33380  opprlidlabs  33670  constrcccllem  34048  constrcbvlem  34049  inelsros  34472  diffiunisros  34473  hgt749d  34940  tgoldbachgt  34954  axtgupdim2ALTV  34959  afsval  34965  brafs  34966  bnj981  35242  bnj1326  35318  cvmlift3lem2  35667  cvmlift3lem4  35669  cvmlift3  35675  brofs  36352  brifs  36390  cgr3permute1  36395  brcolinear2  36405  colineardim1  36408  brfs  36426  btwnconn1  36448  brsegle  36455  unblimceq0  36942  unbdqndv2  36946  rdgeqoa  37861  iscringd  38494  oposlem  39803  ishlat1  39973  3dim1lem5  40087  lvoli2  40202  cdlemk42  41562  diclspsn  41815  monotoddzz  43517  jm2.27  43582  mendlmod  43763  fiiuncl  45642  wessf1ornlem  45760  infleinf  45944  fmulcl  46154  fmuldfeqlem1  46155  fmuldfeq  46156  climinf2mpt  46285  climinfmpt  46286  fprodcncf  46471  dvnmptdivc  46509  dvnprodlem2  46518  dvnprodlem3  46519  stoweidlem6  46577  stoweidlem8  46579  stoweidlem26  46597  stoweidlem31  46602  stoweidlem62  46633  fourierdlem41  46719  fourierdlem48  46725  fourierdlem49  46726  sge0iunmpt  46989  ovnsubaddlem1  47141  isgbe  48370  9gbo  48393  11gbo  48394  sbgoldbst  48397  sbgoldbaltlem1  48398  sbgoldbaltlem2  48399  bgoldbtbndlem4  48427  bgoldbtbnd  48428