Theorem 3anbi3d 1445

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 1441	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  3484  ceqsex4v  3485  ceqsex8v  3487  vtocl3gafOLD  3526  vtocl3gaOLD  3528  mob  3664  offval22  8032  smogt  8301  ttrcleq  9624  cfsmolem  10186  fseq1m1p1  13547  pfxsuff1eqwrdeq  14655  2swrd2eqwrdeq  14909  wrdl3s3  14918  prodmo  15895  fprod  15900  divalg  16366  funcres2b  17858  posi  18277  mhmlem  19032  isdrngrd  20737  isdrngrdOLD  20739  lmodlema  20854  connsub  23399  lmmbr3  25240  lmmcvg  25241  dvmptfsum  25955  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupno  27684  nosupfv  27687  noinfcbv  27698  noinfno  27699  noinffv  27702  bdayfinbndlem2  28477  axtg5seg  28550  axtgupdim2  28556  axtgeucl  28557  ishlg  28687  hlcomb  28688  brbtwn  28985  axlowdim  29047  axeuclidlem  29048  usgr2wlkspth  29845  usgr2pth0  29851  wwlksnwwlksnon  30001  usgrwwlks2on  30044  umgrwwlks2on  30045  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  nvi  30703  isslmd  33281  slmdlema  33282  opprlidlabs  33563  constrcccllem  33917  constrcbvlem  33918  inelsros  34341  diffiunisros  34342  hgt749d  34812  tgoldbachgt  34826  axtgupdim2ALTV  34831  afsval  34834  brafs  34835  bnj981  35111  bnj1326  35187  cvmlift3lem2  35521  cvmlift3lem4  35523  cvmlift3  35529  brofs  36206  brifs  36244  cgr3permute1  36249  brcolinear2  36259  colineardim1  36262  brfs  36280  btwnconn1  36302  brsegle  36309  unblimceq0  36786  unbdqndv2  36790  rdgeqoa  37703  iscringd  38336  oposlem  39645  ishlat1  39815  3dim1lem5  39929  lvoli2  40044  cdlemk42  41404  diclspsn  41657  monotoddzz  43392  jm2.27  43457  mendlmod  43638  fiiuncl  45517  wessf1ornlem  45636  infleinf  45822  fmulcl  46032  fmuldfeqlem1  46033  fmuldfeq  46034  climinf2mpt  46163  climinfmpt  46164  fprodcncf  46349  dvnmptdivc  46387  dvnprodlem2  46396  dvnprodlem3  46397  stoweidlem6  46455  stoweidlem8  46457  stoweidlem26  46475  stoweidlem31  46480  stoweidlem62  46511  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  sge0iunmpt  46867  ovnsubaddlem1  47019  isgbe  48242  9gbo  48265  11gbo  48266  sbgoldbst  48269  sbgoldbaltlem1  48270  sbgoldbaltlem2  48271  bgoldbtbndlem4  48299  bgoldbtbnd  48300