Theorem 3anbi123d 1432

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi3d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))
bi3d.3	⊢ (𝜑 → (𝜂 ↔ 𝜁))

Assertion

Ref	Expression
3anbi123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 632	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1085	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1085	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 316	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anbi12d  1433  3anbi13d  1434  3anbi23d  1435  ax12wdemo  2135  limeq  6198  f13dfv  7025  epne3  7489  oteqimp  7702  wfrlem1  7948  wfrlem15  7963  smoeq  7981  ereq1  8290  indexfi  8826  hartogslem1  9000  tz9.1  9165  updjud  9357  alephval3  9530  cofsmo  9685  cfsmolem  9686  alephsing  9692  axdc3lem2  9867  axdc3lem3  9868  axdc3  9870  axdc4lem  9871  zornn0g  9921  fpwwe2lem5  10050  canthwelem  10066  canthwe  10067  pwfseqlem4a  10077  pwfseqlem4  10078  elwina  10102  elina  10103  iswun  10120  elgrug  10208  iccshftr  12866  iccshftl  12868  iccdil  12870  icccntr  12872  fzaddel  12935  elfzomelpfzo  13135  axdc4uzlem  13345  wrdl1s1  13962  wwlktovf  14314  wwlktovf1  14315  wwlktovfo  14316  wrd2f1tovbij  14318  dfrtrcl2  14415  sqrmo  14605  resqrtcl  14607  resqrtthlem  14608  sqrtneg  14621  sqreu  14714  sqrtthlem  14716  eqsqrtd  14721  prodeq1f  15256  zprod  15285  divalglem10  15747  dfgcd2  15888  coprmprod  15999  pythagtriplem18  16163  pythagtriplem19  16164  prmgaplem3  16383  prmgaplem4  16384  isstruct2  16487  imasval  16778  mreexexlemd  16909  catidd  16945  iscatd2  16946  subsubc  17117  isfunc  17128  funcres2b  17161  ispos  17551  posi  17554  isposd  17559  pospropd  17738  isps  17806  imasmnd2  17942  sgrp2rid2ex  18086  imasgrp2  18208  psgnunilem3  18618  isringd  19329  imasring  19363  isdrngd  19521  islmod  19632  lmodlema  19633  islmodd  19634  lmodprop2d  19690  lmhmpropd  19839  assapropd  20095  isphl  20766  isphld  20792  phlpropd  20793  mdetunilem3  21217  mdetunilem9  21223  fiinopn  21503  iscldtop  21697  lmfval  21834  connsuba  22022  1stcfb  22047  2ndcctbss  22057  subislly  22083  ptval  22172  elpt  22174  elptr  22175  upxp  22225  isfbas  22431  ustval  22805  isust  22806  ustincl  22810  ustdiag  22811  ustinvel  22812  ustexhalf  22813  ust0  22822  imasdsf1olem  22977  tngngp3  23259  lmhmclm  23685  iscph  23768  iscau2  23874  pmltpclem1  24043  isi1f  24269  mbfi1fseqlem6  24315  iblcnlem  24383  dvfsumlem4  24620  aannenlem1  24911  aannenlem2  24912  ulmval  24962  istrkgb  26235  istrkge  26237  istrkgld  26239  istrkg2ld  26240  istrkg3ld  26241  axtgupdim2  26251  axtgeucl  26252  trgcgrg  26295  ishlg  26382  colline  26429  iscgra  26589  isinag  26618  brbtwn  26679  axpaschlem  26720  axlowdim  26741  axeuclid  26743  eengtrkge  26767  issubgr  27047  nb3grpr  27158  nb3grpr2  27159  cplgr3v  27211  wksfval  27385  iswlk  27386  upgr2wlk  27444  wlkiswwlks2  27647  wwlksnextfun  27670  wwlksnextinj  27671  wwlksnextbij  27674  wwlksnextprop  27685  2wlkdlem4  27701  umgr2wlk  27722  umgrwwlks2on  27730  elwspths2spth  27740  isclwwlk  27756  clwlkclwwlklem1  27771  erclwwlkeq  27790  clwwlkn1loopb  27815  erclwwlkneq  27840  s2elclwwlknon2  27877  3wlkdlem5  27936  3wlkdlem6  27938  3wlkdlem9  27941  3wlkdlem10  27942  uhgr3cyclex  27955  upgr4cycl4dv4e  27958  frgr3v  28048  3cyclfrgrrn1  28058  extwwlkfabel  28126  isplig  28247  lpni  28251  isgrpo  28268  vciOLD  28332  isvclem  28348  isnvlem  28381  sspval  28494  isssp  28495  ajfval  28580  dipdir  28613  siilem2  28623  issh  28979  elunop2  29784  superpos  30125  padct  30449  resspos  30641  isslmd  30825  slmdlema  30826  locfinreflem  31099  locfinref  31100  zhmnrg  31203  ismntoplly  31261  issiga  31366  isrnsiga  31367  isldsys  31410  rossros  31434  ismeas  31453  isrnmeas  31454  pmeasmono  31577  pmeasadd  31578  istrkg2d  31932  axtgupdim2ALTV  31934  afsval  31937  brafs  31938  bnj919  32033  bnj976  32044  bnj607  32183  bnj873  32191  cvmlift3lem2  32562  cvmlift3lem6  32566  cvmlift3lem7  32567  cvmlift3lem9  32569  cvmlift3  32570  mclsppslem  32825  dfon2lem1  33023  dfon2lem3  33025  dfon2lem7  33029  frrlem1  33118  frrlem13  33130  nodense  33191  noprefixmo  33197  nosupfv  33201  noetalem5  33216  noeta  33217  brofs  33461  ofscom  33463  btwnouttr  33480  brifs  33499  cgr3com  33509  brcolinear  33515  brfs  33535  unblimceq0lem  33840  knoppndvlem21  33866  csbwrecsg  34602  rdgeqoa  34645  poimirlem4  34890  poimirlem27  34913  mblfinlem3  34925  indexa  35002  sdclem1  35012  fdc  35014  neificl  35022  heiborlem2  35084  isass  35118  ismndo2  35146  isrngo  35169  rngomndo  35207  isgrpda  35227  igenval2  35338  eleqvrels2  35821  eleqvrels3  35822  eqvreleq  35831  lshpset2N  36249  isopos  36310  oposlem  36312  cmtfvalN  36340  cvrfval  36398  3dimlem1  36588  3dim1lem5  36596  lplni2  36667  lvoli2  36711  4atlem11  36739  dalawlem15  37015  cdlemftr3  37695  tendofset  37888  tendoset  37889  istendo  37890  cdlemk28-3  38038  cdlemkid3N  38063  cdlemkid4  38064  lpolsetN  38612  islpolN  38613  lpolconN  38617  ismrc  39291  rabren3dioph  39405  irrapxlem5  39416  rmydioph  39604  mpaaeu  39743  mpaaval  39744  mpaalem  39745  dfsucon  39882  dfrtrcl3  40071  brco3f1o  40376  grumnud  40615  eliooshift  41774  stoweidlem5  42283  stoweidlem18  42296  stoweidlem28  42306  stoweidlem31  42309  stoweidlem41  42319  stoweidlem43  42321  stoweidlem44  42322  stoweidlem45  42323  stoweidlem51  42329  stoweidlem55  42333  stoweidlem59  42337  issal  42592  fundcmpsurbijinjpreimafv  43560  fundcmpsurbijinj  43563  fundcmpsurinjALT  43565  ichnreuop  43627  proththdlem  43771  6gbe  43929  8gbe  43931  bgoldbtbndlem2  43964  bgoldbtbndlem3  43965  bgoldbtbnd  43967  upwlksfval  44003  isupwlk  44004  el0ldep  44514  ldepspr  44521  lmod1  44540  zlmodzxzldep  44552