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

Theorem 3anbi123d 1398
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 747 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 747 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1039 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1039 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 303 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1037
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 386  df-3an 1039
This theorem is referenced by:  3anbi12d  1399  3anbi13d  1400  3anbi23d  1401  ax12wdemo  2011  limeq  5733  f13dfv  6527  epne3  6977  oteqimp  7184  wfrlem1  7411  wfrlem15  7426  smoeq  7444  ereq1  7746  indexfi  8271  hartogslem1  8444  tz9.1  8602  alephval3  8930  cofsmo  9088  cfsmolem  9089  alephsing  9095  axdc3lem2  9270  axdc3lem3  9271  axdc3  9273  axdc4lem  9274  zornn0g  9324  fpwwe2lem5  9453  canthwelem  9469  canthwe  9470  pwfseqlem4a  9480  pwfseqlem4  9481  elwina  9505  elina  9506  iswun  9523  elgrug  9611  iccshftr  12303  iccshftl  12305  iccdil  12307  icccntr  12309  fzaddel  12372  elfzomelpfzo  12568  axdc4uzlem  12777  wrdl1s1  13389  wwlktovf  13693  wwlktovf1  13694  wwlktovfo  13695  wrd2f1tovbij  13697  dfrtrcl2  13796  sqrmo  13986  resqrtcl  13988  resqrtthlem  13989  sqrtneg  14002  sqreu  14094  sqrtthlem  14096  eqsqrtd  14101  prodeq1f  14632  zprod  14661  divalglem10  15119  dfgcd2  15257  coprmprod  15369  pythagtriplem18  15531  pythagtriplem19  15532  prmgaplem3  15751  prmgaplem4  15752  isstruct2  15861  imasval  16165  mreexexlemd  16298  catidd  16335  iscatd2  16336  subsubc  16507  isfunc  16518  funcres2b  16551  ispos  16941  posi  16944  isposd  16949  pospropd  17128  isps  17196  imasmnd2  17321  sgrp2rid2ex  17408  imasgrp2  17524  psgnunilem3  17910  isringd  18579  imasring  18613  isdrngd  18766  islmod  18861  lmodlema  18862  islmodd  18863  lmodprop2d  18919  lmhmpropd  19067  assapropd  19321  isphl  19967  isphld  19993  phlpropd  19994  mdetunilem3  20414  mdetunilem9  20420  fiinopn  20700  iscldtop  20893  lmfval  21030  connsuba  21217  1stcfb  21242  2ndcctbss  21252  subislly  21278  ptval  21367  elpt  21369  elptr  21370  upxp  21420  isfbas  21627  ustval  22000  isust  22001  ustincl  22005  ustdiag  22006  ustinvel  22007  ustexhalf  22008  ust0  22017  imasdsf1olem  22172  tngngp3  22454  lmhmclm  22881  iscph  22964  iscau2  23069  pmltpclem1  23211  isi1f  23435  mbfi1fseqlem6  23481  iblcnlem  23549  dvfsumlem4  23786  aannenlem1  24077  aannenlem2  24078  ulmval  24128  istrkgb  25348  istrkge  25350  istrkgld  25352  istrkg2ld  25353  istrkg3ld  25354  axtgupdim2  25364  axtgeucl  25365  trgcgrg  25404  ishlg  25491  colline  25538  iscgra  25695  isinag  25723  brbtwn  25773  axpaschlem  25814  axlowdim  25835  axeuclid  25837  eengtrkge  25860  issubgr  26157  nb3grpr  26278  nb3grpr2  26279  cplgr3v  26325  wksfval  26499  iswlk  26500  upgr2wlk  26558  wlkiswwlks2  26755  wwlksnextfun  26787  wwlksnextinj  26788  wwlksnextbij  26791  wwlksnextprop  26801  2wlkdlem4  26818  umgr2wlk  26839  umgrwwlks2on  26844  elwspths2spth  26856  isclwwlks  26874  clwlkclwwlklem1  26894  erclwwlkseq  26925  erclwwlksneq  26937  3wlkdlem5  27016  3wlkdlem6  27018  3wlkdlem9  27021  3wlkdlem10  27022  uhgr3cyclex  27035  upgr4cycl4dv4e  27038  frgr3v  27132  3cyclfrgrrn1  27142  numclwlk1lem2foa  27208  numclwlk1lem2f  27209  isplig  27312  lpni  27316  isgrpo  27335  vciOLD  27400  isvclem  27416  isnvlem  27449  sspval  27562  isssp  27563  ajfval  27648  dipdir  27681  siilem2  27691  issh  28049  elunop2  28856  superpos  29197  padct  29482  resspos  29644  isslmd  29740  slmdlema  29741  locfinreflem  29892  locfinref  29893  zhmnrg  29996  ismntoplly  30054  issiga  30159  isrnsigaOLD  30160  isrnsiga  30161  isldsys  30204  rossros  30228  ismeas  30247  isrnmeas  30248  pmeasmono  30371  pmeasadd  30372  istrkg2d  30729  axtgupdim2OLD  30731  afsval  30734  brafs  30735  bnj919  30822  bnj976  30833  bnj607  30971  bnj873  30979  cvmlift3lem2  31287  cvmlift3lem6  31291  cvmlift3lem7  31292  cvmlift3lem9  31294  cvmlift3  31295  mclsppslem  31465  dfon2lem1  31672  dfon2lem3  31674  dfon2lem7  31678  frrlem1  31764  nodense  31826  noprefixmo  31832  nosupfv  31836  noetalem5  31851  noeta  31852  brofs  32096  ofscom  32098  btwnouttr  32115  brifs  32134  cgr3com  32144  brcolinear  32150  brfs  32170  unblimceq0lem  32481  knoppndvlem21  32507  csbwrecsg  33153  rdgeqoa  33198  poimirlem4  33393  poimirlem27  33416  mblfinlem3  33428  indexa  33508  sdclem1  33519  fdc  33521  neificl  33529  heiborlem2  33591  isass  33625  ismndo2  33653  isrngo  33676  rngomndo  33714  isgrpda  33734  igenval2  33845  lshpset2N  34232  isopos  34293  oposlem  34295  cmtfvalN  34323  cvrfval  34381  3dimlem1  34570  3dim1lem5  34578  lplni2  34649  lvoli2  34693  4atlem11  34721  dalawlem15  34997  cdlemftr3  35679  tendofset  35872  tendoset  35873  istendo  35874  cdlemk28-3  36022  cdlemkid3N  36047  cdlemkid4  36048  lpolsetN  36597  islpolN  36598  lpolconN  36602  ismrc  37090  rabren3dioph  37205  irrapxlem5  37216  rmydioph  37407  mpaaeu  37546  mpaaval  37547  mpaalem  37548  dfrtrcl3  37851  brco3f1o  38157  eliooshift  39538  stoweidlem5  39991  stoweidlem18  40004  stoweidlem28  40014  stoweidlem31  40017  stoweidlem41  40027  stoweidlem43  40029  stoweidlem44  40030  stoweidlem45  40031  stoweidlem51  40037  stoweidlem55  40041  stoweidlem59  40045  issal  40303  proththdlem  41301  6gbe  41430  8gbe  41432  bgoldbtbndlem2  41465  bgoldbtbndlem3  41466  bgoldbtbnd  41468  upwlksfval  41487  isupwlk  41488  el0ldep  42026  ldepspr  42033  lmod1  42052  zlmodzxzldep  42064
  Copyright terms: Public domain W3C validator