Theorem 3anbi3d 1440

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  ceqsex3v  3530  ceqsex4v  3531  ceqsex8v  3533  vtocl3gaf  3568  vtocl3ga  3569  mob  3712  offval22  8076  smogt  8369  ttrcleq  9706  cfsmolem  10267  fseq1m1p1  13580  pfxsuff1eqwrdeq  14653  2swrd2eqwrdeq  14908  wrdl3s3  14917  prodmo  15884  fprod  15889  divalg  16350  funcres2b  17851  posi  18274  mhmlem  18981  isdrngrd  20534  isdrngrdOLD  20536  lmodlema  20619  connsub  23145  lmmbr3  25008  lmmcvg  25009  dvmptfsum  25727  nosupprefixmo  27439  noinfprefixmo  27440  nosupcbv  27441  nosupno  27442  nosupfv  27445  noinfcbv  27456  noinfno  27457  noinffv  27460  axtg5seg  27983  axtgupdim2  27989  axtgeucl  27990  ishlg  28120  hlcomb  28121  brbtwn  28424  axlowdim  28486  axeuclidlem  28487  usgr2wlkspth  29283  usgr2pth0  29289  wwlksnwwlksnon  29436  umgrwwlks2on  29478  upgr3v3e3cycl  29700  upgr4cycl4dv4e  29705  nvi  30134  isslmd  32617  slmdlema  32618  opprlidlabs  32873  inelsros  33474  diffiunisros  33475  hgt749d  33959  tgoldbachgt  33973  axtgupdim2ALTV  33978  afsval  33981  brafs  33982  bnj981  34259  bnj1326  34335  cvmlift3lem2  34609  cvmlift3lem4  34611  cvmlift3  34617  brofs  35281  brifs  35319  cgr3permute1  35324  brcolinear2  35334  colineardim1  35337  brfs  35355  btwnconn1  35377  brsegle  35384  unblimceq0  35686  unbdqndv2  35690  rdgeqoa  36554  iscringd  37169  oposlem  38355  ishlat1  38525  3dim1lem5  38640  lvoli2  38755  cdlemk42  40115  diclspsn  40368  monotoddzz  41984  jm2.27  42049  mendlmod  42237  fiiuncl  44053  wessf1ornlem  44182  infleinf  44380  fmulcl  44595  fmuldfeqlem1  44596  fmuldfeq  44597  climinf2mpt  44728  climinfmpt  44729  fprodcncf  44914  dvnmptdivc  44952  dvnprodlem2  44961  dvnprodlem3  44962  stoweidlem6  45020  stoweidlem8  45022  stoweidlem26  45040  stoweidlem31  45045  stoweidlem62  45076  fourierdlem41  45162  fourierdlem48  45168  fourierdlem49  45169  sge0iunmpt  45432  ovnsubaddlem1  45584  isgbe  46717  9gbo  46740  11gbo  46741  sbgoldbst  46744  sbgoldbaltlem1  46745  sbgoldbaltlem2  46746  bgoldbtbndlem4  46774  bgoldbtbnd  46775