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

Theorem 3anbi123d 1560
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 624 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 624 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1109 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1109 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 305 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3anbi12d  1561  3anbi13d  1562  3anbi23d  1563  ax12wdemo  2177  limeq  5920  f13dfv  6722  epne3  7178  oteqimp  7385  wfrlem1  7617  wfrlem15  7633  smoeq  7651  ereq1  7954  indexfi  8481  hartogslem1  8654  tz9.1  8820  updjud  9011  alephval3  9184  cofsmo  9344  cfsmolem  9345  alephsing  9351  axdc3lem2  9526  axdc3lem3  9527  axdc3  9529  axdc4lem  9530  zornn0g  9580  fpwwe2lem5  9709  canthwelem  9725  canthwe  9726  pwfseqlem4a  9736  pwfseqlem4  9737  elwina  9761  elina  9762  iswun  9779  elgrug  9867  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  fzaddel  12582  elfzomelpfzo  12780  axdc4uzlem  12990  wrdl1s1  13585  wwlktovf  13986  wwlktovf1  13987  wwlktovfo  13988  wrd2f1tovbij  13990  dfrtrcl2  14087  sqrmo  14277  resqrtcl  14279  resqrtthlem  14280  sqrtneg  14293  sqreu  14385  sqrtthlem  14387  eqsqrtd  14392  prodeq1f  14921  zprod  14950  divalglem10  15407  dfgcd2  15544  coprmprod  15655  pythagtriplem18  15816  pythagtriplem19  15817  prmgaplem3  16036  prmgaplem4  16037  isstruct2  16140  imasval  16437  mreexexlemd  16570  catidd  16606  iscatd2  16607  subsubc  16778  isfunc  16789  funcres2b  16822  ispos  17213  posi  17216  isposd  17221  pospropd  17400  isps  17468  imasmnd2  17593  sgrp2rid2ex  17681  imasgrp2  17797  psgnunilem3  18180  isringd  18852  imasring  18886  isdrngd  19041  islmod  19136  lmodlema  19137  islmodd  19138  lmodprop2d  19194  lmhmpropd  19345  assapropd  19601  isphl  20248  isphld  20274  phlpropd  20275  mdetunilem3  20697  mdetunilem9  20703  fiinopn  20985  iscldtop  21179  lmfval  21316  connsuba  21503  1stcfb  21528  2ndcctbss  21538  subislly  21564  ptval  21653  elpt  21655  elptr  21656  upxp  21706  isfbas  21912  ustval  22285  isust  22286  ustincl  22290  ustdiag  22291  ustinvel  22292  ustexhalf  22293  ust0  22302  imasdsf1olem  22457  tngngp3  22739  lmhmclm  23165  iscph  23248  iscau2  23354  pmltpclem1  23506  isi1f  23732  mbfi1fseqlem6  23778  iblcnlem  23846  dvfsumlem4  24083  aannenlem1  24374  aannenlem2  24375  ulmval  24425  istrkgb  25645  istrkge  25647  istrkgld  25649  istrkg2ld  25650  istrkg3ld  25651  axtgupdim2  25661  axtgeucl  25662  trgcgrg  25701  ishlg  25788  colline  25835  iscgra  25992  isinag  26020  brbtwn  26070  axpaschlem  26111  axlowdim  26132  axeuclid  26134  eengtrkge  26157  issubgr  26442  nb3grpr  26563  nb3grpr2  26564  cplgr3v  26622  wksfval  26796  iswlk  26797  upgr2wlk  26855  wlkiswwlks2  27066  wwlksnextfun  27104  wwlksnextinj  27105  wwlksnextfunOLD  27109  wwlksnextinjOLD  27110  wwlksnextbij  27113  wwlksnextbijOLD  27114  wwlksnextprop  27130  wwlksnextpropOLD  27131  2wlkdlem4  27151  umgr2wlk  27172  umgrwwlks2on  27181  elwspths2spth  27192  isclwwlk  27211  clwlkclwwlklem1  27226  erclwwlkeq  27254  clwwlkn1loopb  27286  erclwwlkneq  27319  s2elclwwlknon2  27377  3wlkdlem5  27441  3wlkdlem6  27443  3wlkdlem9  27446  3wlkdlem10  27447  uhgr3cyclex  27460  upgr4cycl4dv4e  27463  frgr3v  27555  3cyclfrgrrn1  27565  extwwlkfabel  27643  extwwlkfabelOLD  27644  isplig  27787  lpni  27791  isgrpo  27808  vciOLD  27872  isvclem  27888  isnvlem  27921  sspval  28034  isssp  28035  ajfval  28120  dipdir  28153  siilem2  28163  issh  28521  elunop2  29328  superpos  29669  padct  29946  resspos  30106  isslmd  30202  slmdlema  30203  locfinreflem  30354  locfinref  30355  zhmnrg  30458  ismntoplly  30516  issiga  30621  isrnsigaOLD  30622  isrnsiga  30623  isldsys  30666  rossros  30690  ismeas  30709  isrnmeas  30710  pmeasmono  30833  pmeasadd  30834  istrkg2d  31195  axtgupdim2OLD  31197  afsval  31200  brafs  31201  bnj919  31285  bnj976  31296  bnj607  31434  bnj873  31442  cvmlift3lem2  31750  cvmlift3lem6  31754  cvmlift3lem7  31755  cvmlift3lem9  31757  cvmlift3  31758  mclsppslem  31928  dfon2lem1  32131  dfon2lem3  32133  dfon2lem7  32137  frrlem1  32224  nodense  32286  noprefixmo  32292  nosupfv  32296  noetalem5  32311  noeta  32312  brofs  32556  ofscom  32558  btwnouttr  32575  brifs  32594  cgr3com  32604  brcolinear  32610  brfs  32630  unblimceq0lem  32936  knoppndvlem21  32962  csbwrecsg  33607  rdgeqoa  33651  poimirlem4  33837  poimirlem27  33860  mblfinlem3  33872  indexa  33951  sdclem1  33961  fdc  33963  neificl  33971  heiborlem2  34033  isass  34067  ismndo2  34095  isrngo  34118  rngomndo  34156  isgrpda  34176  igenval2  34287  eleqvrels2  34765  eleqvrels3  34766  eqvreleq  34773  lshpset2N  35075  isopos  35136  oposlem  35138  cmtfvalN  35166  cvrfval  35224  3dimlem1  35414  3dim1lem5  35422  lplni2  35493  lvoli2  35537  4atlem11  35565  dalawlem15  35841  cdlemftr3  36521  tendofset  36714  tendoset  36715  istendo  36716  cdlemk28-3  36864  cdlemkid3N  36889  cdlemkid4  36890  lpolsetN  37438  islpolN  37439  lpolconN  37443  ismrc  37942  rabren3dioph  38057  irrapxlem5  38068  rmydioph  38258  mpaaeu  38397  mpaaval  38398  mpaalem  38399  dfrtrcl3  38700  brco3f1o  39005  eliooshift  40371  stoweidlem5  40859  stoweidlem18  40872  stoweidlem28  40882  stoweidlem31  40885  stoweidlem41  40895  stoweidlem43  40897  stoweidlem44  40898  stoweidlem45  40899  stoweidlem51  40905  stoweidlem55  40909  stoweidlem59  40913  issal  41171  proththdlem  42206  6gbe  42335  8gbe  42337  bgoldbtbndlem2  42370  bgoldbtbndlem3  42371  bgoldbtbnd  42373  upwlksfval  42385  isupwlk  42386  el0ldep  42924  ldepspr  42931  lmod1  42950  zlmodzxzldep  42962
  Copyright terms: Public domain W3C validator