MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi123d Structured version   Visualization version   GIF version

Theorem 3anbi123d 1547
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
StepHypRef Expression
1 bi3d.1 . . . 4 (𝜑 → (𝜓𝜒))
2 bi3d.2 . . . 4 (𝜑 → (𝜃𝜏))
31, 2anbi12d 616 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 616 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1073 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1073 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 303 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  3anbi12d  1548  3anbi13d  1549  3anbi23d  1550  ax12wdemo  2167  limeq  5878  f13dfv  6673  epne3  7127  oteqimp  7334  wfrlem1  7566  wfrlem15  7582  smoeq  7600  ereq1  7903  indexfi  8430  hartogslem1  8603  tz9.1  8769  updjud  8960  alephval3  9133  cofsmo  9293  cfsmolem  9294  alephsing  9300  axdc3lem2  9475  axdc3lem3  9476  axdc3  9478  axdc4lem  9479  zornn0g  9529  fpwwe2lem5  9658  canthwelem  9674  canthwe  9675  pwfseqlem4a  9685  pwfseqlem4  9686  elwina  9710  elina  9711  iswun  9728  elgrug  9816  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  fzaddel  12582  elfzomelpfzo  12780  axdc4uzlem  12990  wrdl1s1  13594  wwlktovf  13909  wwlktovf1  13910  wwlktovfo  13911  wrd2f1tovbij  13913  dfrtrcl2  14010  sqrmo  14200  resqrtcl  14202  resqrtthlem  14203  sqrtneg  14216  sqreu  14308  sqrtthlem  14310  eqsqrtd  14315  prodeq1f  14845  zprod  14874  divalglem10  15333  dfgcd2  15471  coprmprod  15582  pythagtriplem18  15744  pythagtriplem19  15745  prmgaplem3  15964  prmgaplem4  15965  isstruct2  16074  imasval  16379  mreexexlemd  16512  catidd  16548  iscatd2  16549  subsubc  16720  isfunc  16731  funcres2b  16764  ispos  17155  posi  17158  isposd  17163  pospropd  17342  isps  17410  imasmnd2  17535  sgrp2rid2ex  17622  imasgrp2  17738  psgnunilem3  18123  isringd  18793  imasring  18827  isdrngd  18982  islmod  19077  lmodlema  19078  islmodd  19079  lmodprop2d  19135  lmhmpropd  19286  assapropd  19542  isphl  20190  isphld  20216  phlpropd  20217  mdetunilem3  20638  mdetunilem9  20644  fiinopn  20926  iscldtop  21120  lmfval  21257  connsuba  21444  1stcfb  21469  2ndcctbss  21479  subislly  21505  ptval  21594  elpt  21596  elptr  21597  upxp  21647  isfbas  21853  ustval  22226  isust  22227  ustincl  22231  ustdiag  22232  ustinvel  22233  ustexhalf  22234  ust0  22243  imasdsf1olem  22398  tngngp3  22680  lmhmclm  23106  iscph  23189  iscau2  23294  pmltpclem1  23436  isi1f  23661  mbfi1fseqlem6  23707  iblcnlem  23775  dvfsumlem4  24012  aannenlem1  24303  aannenlem2  24304  ulmval  24354  istrkgb  25575  istrkge  25577  istrkgld  25579  istrkg2ld  25580  istrkg3ld  25581  axtgupdim2  25591  axtgeucl  25592  trgcgrg  25631  ishlg  25718  colline  25765  iscgra  25922  isinag  25950  brbtwn  26000  axpaschlem  26041  axlowdim  26062  axeuclid  26064  eengtrkge  26087  issubgr  26386  nb3grpr  26507  nb3grpr2  26508  cplgr3v  26566  wksfval  26740  iswlk  26741  upgr2wlk  26799  wlkiswwlks2  27009  wwlksnextfun  27042  wwlksnextinj  27043  wwlksnextbij  27046  wwlksnextprop  27057  2wlkdlem4  27075  umgr2wlk  27096  umgrwwlks2on  27105  elwspths2spth  27116  isclwwlk  27134  clwlkclwwlklem1  27149  erclwwlkeq  27168  clwwlkn1loopb  27199  erclwwlkneq  27225  s2elclwwlknon2  27279  3wlkdlem5  27343  3wlkdlem6  27345  3wlkdlem9  27348  3wlkdlem10  27349  uhgr3cyclex  27362  upgr4cycl4dv4e  27365  frgr3v  27457  3cyclfrgrrn1  27467  extwwlkfabel  27539  isplig  27670  lpni  27674  isgrpo  27691  vciOLD  27756  isvclem  27772  isnvlem  27805  sspval  27918  isssp  27919  ajfval  28004  dipdir  28037  siilem2  28047  issh  28405  elunop2  29212  superpos  29553  padct  29837  resspos  29999  isslmd  30095  slmdlema  30096  locfinreflem  30247  locfinref  30248  zhmnrg  30351  ismntoplly  30409  issiga  30514  isrnsigaOLD  30515  isrnsiga  30516  isldsys  30559  rossros  30583  ismeas  30602  isrnmeas  30603  pmeasmono  30726  pmeasadd  30727  istrkg2d  31084  axtgupdim2OLD  31086  afsval  31089  brafs  31090  bnj919  31175  bnj976  31186  bnj607  31324  bnj873  31332  cvmlift3lem2  31640  cvmlift3lem6  31644  cvmlift3lem7  31645  cvmlift3lem9  31647  cvmlift3  31648  mclsppslem  31818  dfon2lem1  32024  dfon2lem3  32026  dfon2lem7  32030  frrlem1  32117  nodense  32179  noprefixmo  32185  nosupfv  32189  noetalem5  32204  noeta  32205  brofs  32449  ofscom  32451  btwnouttr  32468  brifs  32487  cgr3com  32497  brcolinear  32503  brfs  32523  unblimceq0lem  32834  knoppndvlem21  32860  csbwrecsg  33510  rdgeqoa  33555  poimirlem4  33746  poimirlem27  33769  mblfinlem3  33781  indexa  33860  sdclem1  33871  fdc  33873  neificl  33881  heiborlem2  33943  isass  33977  ismndo2  34005  isrngo  34028  rngomndo  34066  isgrpda  34086  igenval2  34197  lshpset2N  34928  isopos  34989  oposlem  34991  cmtfvalN  35019  cvrfval  35077  3dimlem1  35266  3dim1lem5  35274  lplni2  35345  lvoli2  35389  4atlem11  35417  dalawlem15  35693  cdlemftr3  36374  tendofset  36567  tendoset  36568  istendo  36569  cdlemk28-3  36717  cdlemkid3N  36742  cdlemkid4  36743  lpolsetN  37292  islpolN  37293  lpolconN  37297  ismrc  37790  rabren3dioph  37905  irrapxlem5  37916  rmydioph  38107  mpaaeu  38246  mpaaval  38247  mpaalem  38248  dfrtrcl3  38551  brco3f1o  38857  eliooshift  40250  stoweidlem5  40739  stoweidlem18  40752  stoweidlem28  40762  stoweidlem31  40765  stoweidlem41  40775  stoweidlem43  40777  stoweidlem44  40778  stoweidlem45  40779  stoweidlem51  40785  stoweidlem55  40789  stoweidlem59  40793  issal  41051  proththdlem  42058  6gbe  42187  8gbe  42189  bgoldbtbndlem2  42222  bgoldbtbndlem3  42223  bgoldbtbnd  42225  upwlksfval  42244  isupwlk  42245  el0ldep  42783  ldepspr  42790  lmod1  42809  zlmodzxzldep  42821
  Copyright terms: Public domain W3C validator