Theorem 3anbi123d 1436

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 631	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 631	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1089	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1089	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 313	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anbi12d  1437  3anbi13d  1438  3anbi23d  1439  ax12wdemo  2131  limeq  6376  f13dfv  7274  epne3  7762  oteqimp  7996  xpord2lem  8130  poxp2  8131  xpord3lem  8137  xpord3pred  8140  csbfrecsg  8271  frrlem1  8273  frrlem13  8285  wfrlem1OLD  8310  wfrlem15OLD  8325  smoeq  8352  on2ind  8670  on3ind  8671  naddasslem1  8695  naddasslem2  8696  naddass  8697  ereq1  8712  sbthfi  9204  indexfi  9362  hartogslem1  9539  brttrcl2  9711  ssttrcl  9712  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  tz9.1  9726  updjud  9931  alephval3  10107  cofsmo  10266  cfsmolem  10267  alephsing  10273  axdc3lem2  10448  axdc3lem3  10449  axdc3  10451  axdc4lem  10452  zornn0g  10502  fpwwe2lem4  10631  canthwelem  10647  canthwe  10648  pwfseqlem4a  10658  pwfseqlem4  10659  elwina  10683  elina  10684  iswun  10701  elgrug  10789  iccshftr  13465  iccshftl  13467  iccdil  13469  icccntr  13471  fzaddel  13537  elfzomelpfzo  13738  axdc4uzlem  13950  wrdl1s1  14566  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  wrd2f1tovbij  14913  dfrtrcl2  15011  sqrmo  15200  resqrtcl  15202  resqrtthlem  15203  sqrtneg  15216  sqreu  15309  sqrtthlem  15311  eqsqrtd  15316  prodeq1f  15854  zprod  15883  divalglem10  16347  dfgcd2  16490  coprmprod  16600  pythagtriplem18  16767  pythagtriplem19  16768  prmgaplem3  16988  prmgaplem4  16989  isstruct2  17084  imasval  17459  mreexexlemd  17590  catidd  17626  iscatd2  17627  subsubc  17805  isfunc  17816  funcres2b  17849  ispos  18269  posi  18272  isposd  18278  pospropd  18282  isps  18523  imasmnd2  18664  sgrp2rid2ex  18810  imasgrp2  18940  psgnunilem3  19366  isringd  20107  imasring  20147  isdrngd  20394  isdrngdOLD  20396  islmod  20479  lmodlema  20480  islmodd  20481  lmodprop2d  20539  lmhmpropd  20689  isphl  21187  isphld  21213  phlpropd  21214  mdetunilem3  22123  mdetunilem9  22129  fiinopn  22410  iscldtop  22606  lmfval  22743  connsuba  22931  1stcfb  22956  2ndcctbss  22966  subislly  22992  ptval  23081  elpt  23083  elptr  23084  upxp  23134  isfbas  23340  ustval  23714  isust  23715  ustincl  23719  ustdiag  23720  ustinvel  23721  ustexhalf  23722  ust0  23731  imasdsf1olem  23886  tngngp3  24180  lmhmclm  24610  iscph  24694  iscau2  24801  pmltpclem1  24972  isi1f  25198  mbfi1fseqlem6  25245  iblcnlem  25313  dvfsumlem4  25553  aannenlem1  25848  aannenlem2  25849  ulmval  25899  nodense  27202  nosupprefixmo  27210  noinfprefixmo  27211  nosupcbv  27212  nosupfv  27216  noinfcbv  27227  noinffv  27231  noetalem2  27252  eqscut  27314  no2indslem  27447  no3inds  27451  addsproplem3  27464  negsproplem3  27514  mulsproplem10  27591  istrkgb  27744  istrkge  27746  istrkgld  27748  istrkg2ld  27749  istrkg3ld  27750  axtgupdim2  27760  axtgeucl  27761  trgcgrg  27804  ishlg  27891  colline  27938  iscgra  28098  isinag  28127  brbtwn  28195  axpaschlem  28236  axlowdim  28257  axeuclid  28259  eengtrkge  28283  issubgr  28566  nb3grpr  28677  nb3grpr2  28678  cplgr3v  28730  wksfval  28904  iswlk  28905  upgr2wlk  28963  wlkiswwlks2  29167  wwlksnextfun  29190  wwlksnextinj  29191  wwlksnextbij  29194  wwlksnextprop  29204  2wlkdlem4  29220  umgr2wlk  29241  umgrwwlks2on  29249  elwspths2spth  29259  isclwwlk  29275  clwlkclwwlklem1  29290  erclwwlkeq  29309  clwwlkn1loopb  29334  erclwwlkneq  29358  s2elclwwlknon2  29395  3wlkdlem5  29454  3wlkdlem6  29456  3wlkdlem9  29459  3wlkdlem10  29460  uhgr3cyclex  29473  upgr4cycl4dv4e  29476  frgr3v  29566  3cyclfrgrrn1  29576  extwwlkfabel  29644  isplig  29767  lpni  29771  isgrpo  29788  vciOLD  29852  isvclem  29868  isnvlem  29901  sspval  30014  isssp  30015  ajfval  30100  dipdir  30133  siilem2  30143  issh  30499  elunop2  31304  superpos  31645  padct  31982  resspos  32174  isslmd  32388  slmdlema  32389  elrspunidl  32591  locfinreflem  32889  locfinref  32890  zarcmplem  32930  zhmnrg  33016  ismntoplly  33074  issiga  33179  isrnsiga  33180  isldsys  33223  rossros  33247  ismeas  33266  isrnmeas  33267  pmeasmono  33392  pmeasadd  33393  istrkg2d  33747  axtgupdim2ALTV  33749  afsval  33752  brafs  33753  bnj919  33847  bnj976  33857  bnj607  33996  bnj873  34004  cvmlift3lem2  34380  cvmlift3lem6  34384  cvmlift3lem7  34385  cvmlift3lem9  34387  cvmlift3  34388  mclsppslem  34643  dfon2lem1  34824  dfon2lem3  34826  dfon2lem7  34830  brofs  35046  ofscom  35048  btwnouttr  35065  brifs  35084  cgr3com  35094  brcolinear  35100  brfs  35120  unblimceq0lem  35468  knoppndvlem21  35494  rdgeqoa  36337  poimirlem4  36578  poimirlem27  36601  mblfinlem3  36613  indexa  36687  sdclem1  36697  fdc  36699  neificl  36707  heiborlem2  36766  isass  36800  ismndo2  36828  isrngo  36851  rngomndo  36889  isgrpda  36909  igenval2  37020  eleqvrels2  37548  eleqvrels3  37549  eqvreleq  37558  lshpset2N  38075  isopos  38136  oposlem  38138  cmtfvalN  38166  cvrfval  38224  3dimlem1  38415  3dim1lem5  38423  lplni2  38494  lvoli2  38538  4atlem11  38566  dalawlem15  38842  cdlemftr3  39522  tendofset  39715  tendoset  39716  istendo  39717  cdlemk28-3  39865  cdlemkid3N  39890  cdlemkid4  39891  lpolsetN  40439  islpolN  40440  lpolconN  40444  ismrc  41521  rabren3dioph  41635  irrapxlem5  41646  rmydioph  41835  mpaaeu  41974  mpaaval  41975  mpaalem  41976  naddwordnexlem4  42234  dfsucon  42356  minregex  42367  dfrtrcl3  42566  brco3f1o  42866  grumnud  43127  eliooshift  44298  stoweidlem5  44800  stoweidlem18  44813  stoweidlem28  44823  stoweidlem31  44826  stoweidlem41  44836  stoweidlem43  44838  stoweidlem44  44839  stoweidlem45  44840  stoweidlem51  44846  stoweidlem55  44850  stoweidlem59  44854  issal  45109  fundcmpsurbijinjpreimafv  46154  fundcmpsurbijinj  46157  fundcmpsurinjALT  46159  ichnreuop  46219  proththdlem  46360  6gbe  46518  8gbe  46520  bgoldbtbndlem2  46553  bgoldbtbndlem3  46554  bgoldbtbnd  46556  upwlksfval  46592  isupwlk  46593  isrngd  46751  imasrng  46757  subrngpropd  46826  el0ldep  47225  ldepspr  47232  lmod1  47251  zlmodzxzldep  47263  catprs  47709  catprsc  47711  prsthinc  47752