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  3493  ceqsex4v  3494  ceqsex8v  3496  vtocl3gafOLD  3535  vtocl3gaOLD  3537  mob  3673  offval22  8028  smogt  8297  ttrcleq  9616  cfsmolem  10178  fseq1m1p1  13513  pfxsuff1eqwrdeq  14620  2swrd2eqwrdeq  14874  wrdl3s3  14883  prodmo  15857  fprod  15862  divalg  16328  funcres2b  17819  posi  18238  mhmlem  18990  isdrngrd  20697  isdrngrdOLD  20699  lmodlema  20814  connsub  23363  lmmbr3  25214  lmmcvg  25215  dvmptfsum  25933  nosupprefixmo  27666  noinfprefixmo  27667  nosupcbv  27668  nosupno  27669  nosupfv  27672  noinfcbv  27683  noinfno  27684  noinffv  27687  axtg5seg  28486  axtgupdim2  28492  axtgeucl  28493  ishlg  28623  hlcomb  28624  brbtwn  28921  axlowdim  28983  axeuclidlem  28984  usgr2wlkspth  29781  usgr2pth0  29787  wwlksnwwlksnon  29937  usgrwwlks2on  29980  umgrwwlks2on  29981  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  nvi  30638  isslmd  33233  slmdlema  33234  opprlidlabs  33515  constrcccllem  33860  constrcbvlem  33861  inelsros  34284  diffiunisros  34285  hgt749d  34755  tgoldbachgt  34769  axtgupdim2ALTV  34774  afsval  34777  brafs  34778  bnj981  35055  bnj1326  35131  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3  35471  brofs  36148  brifs  36186  cgr3permute1  36191  brcolinear2  36201  colineardim1  36204  brfs  36222  btwnconn1  36244  brsegle  36251  unblimceq0  36650  unbdqndv2  36654  rdgeqoa  37514  iscringd  38138  oposlem  39381  ishlat1  39551  3dim1lem5  39665  lvoli2  39780  cdlemk42  41140  diclspsn  41393  monotoddzz  43127  jm2.27  43192  mendlmod  43373  fiiuncl  45252  wessf1ornlem  45371  infleinf  45558  fmulcl  45769  fmuldfeqlem1  45770  fmuldfeq  45771  climinf2mpt  45900  climinfmpt  45901  fprodcncf  46086  dvnmptdivc  46124  dvnprodlem2  46133  dvnprodlem3  46134  stoweidlem6  46192  stoweidlem8  46194  stoweidlem26  46212  stoweidlem31  46217  stoweidlem62  46248  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  sge0iunmpt  46604  ovnsubaddlem1  46756  isgbe  47939  9gbo  47962  11gbo  47963  sbgoldbst  47966  sbgoldbaltlem1  47967  sbgoldbaltlem2  47968  bgoldbtbndlem4  47996  bgoldbtbnd  47997