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

Theorem 3anbi123d 1391
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 743 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 743 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1033 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1033 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 302 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  3anbi12d  1392  3anbi13d  1393  3anbi23d  1394  ax12wdemo  1999  limeq  5652  f13dfv  6430  epne3  6872  oteqimp  7078  wfrlem1  7301  wfrlem15  7316  smoeq  7334  ereq1  7636  indexfi  8157  hartogslem1  8330  tz9.1  8488  alephval3  8816  cofsmo  8974  cfsmolem  8975  alephsing  8981  axdc3lem2  9156  axdc3lem3  9157  axdc3  9159  axdc4lem  9160  zornn0g  9210  fpwwe2lem5  9335  canthwelem  9351  canthwe  9352  pwfseqlem4a  9362  pwfseqlem4  9363  elwina  9387  elina  9388  iswun  9405  elgrug  9493  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzaddel  12246  elfzomelpfzo  12438  axdc4uzlem  12644  wrdl1s1  13247  wwlktovf  13547  wwlktovf1  13548  wwlktovfo  13549  wrd2f1tovbij  13551  dfrtrcl2  13650  sqrmo  13840  resqrtcl  13842  resqrtthlem  13843  sqrtneg  13856  sqreu  13948  sqrtthlem  13950  eqsqrtd  13955  prodeq1f  14477  zprod  14506  divalglem10  14963  dfgcd2  15101  coprmprod  15213  pythagtriplem18  15375  pythagtriplem19  15376  prmgaplem3  15595  prmgaplem4  15596  isstruct2  15704  imasval  15994  mreexexlemd  16127  catidd  16164  iscatd2  16165  subsubc  16336  isfunc  16347  funcres2b  16380  ispos  16770  posi  16773  isposd  16778  pospropd  16957  isps  17025  imasmnd2  17150  sgrp2rid2ex  17237  imasgrp2  17353  psgnunilem3  17739  isringd  18408  imasring  18442  isdrngd  18595  islmod  18690  lmodlema  18691  islmodd  18692  lmodprop2d  18748  lmhmpropd  18894  assapropd  19148  isphl  19792  isphld  19818  phlpropd  19819  mdetunilem3  20239  mdetunilem9  20245  fiinopn  20531  iscldtop  20709  lmfval  20846  consuba  21033  1stcfb  21058  2ndcctbss  21068  subislly  21094  ptval  21183  elpt  21185  elptr  21186  upxp  21236  isfbas  21443  ustval  21816  isust  21817  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  imasdsf1olem  21988  tngngp3  22270  lmhmclm  22695  iscph  22778  iscau2  22883  pmltpclem1  23024  isi1f  23247  mbfi1fseqlem6  23293  iblcnlem  23361  dvfsumlem4  23596  aannenlem1  23887  aannenlem2  23888  ulmval  23938  istrkgb  25154  istrkge  25156  istrkgld  25158  istrkg2ld  25159  istrkg3ld  25160  axtgupdim2  25170  axtgeucl  25171  trgcgrg  25210  ishlg  25297  colline  25344  iscgra  25501  isinag  25529  brbtwn  25579  axpaschlem  25620  axlowdim  25641  axeuclid  25643  eengtrkge  25666  structvtxvallem  25697  nb3grapr  25982  nb3grapr2  25983  cusgra3v  25993  wlks  26047  iswlk  26048  wlkcompim  26054  wlkelwrd  26058  iswlkon  26062  istrl  26067  wlkntrl  26092  is2wlk  26095  ispth  26098  2pthoncl  26133  usg2wlk  26145  3v3e3cycl1  26172  constr3trllem5  26182  constr3cyclpe  26191  4cycl4dv4e  26196  wlkiswwlk2  26225  wwlkextfun  26257  wwlkextinj  26258  wwlkextbij  26261  wwlkextprop  26272  clwlkisclwwlklem2  26314  erclwwlkeq  26339  erclwwlkneq  26351  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  iseupa  26492  eupa0  26501  eupares  26502  eupap1  26503  frgra3v  26529  3cyclfrgrarn1  26539  2spotdisj  26588  numclwlk1lem2foa  26618  isplig  26720  lpni  26722  isgrpo  26735  vciOLD  26800  isvclem  26816  isnvlem  26849  sspval  26962  isssp  26963  ajfval  27048  dipdir  27081  siilem2  27091  issh  27449  elunop2  28256  superpos  28597  padct  28885  resspos  28990  isslmd  29086  slmdlema  29087  locfinreflem  29235  locfinref  29236  zhmnrg  29339  ismntoplly  29397  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503  isldsys  29546  rossros  29570  ismeas  29589  isrnmeas  29590  pmeasmono  29713  pmeasadd  29714  istrkg2d  29997  axtgupdim2OLD  29999  afsval  30002  brafs  30003  bnj919  30091  bnj976  30102  bnj607  30240  bnj873  30248  cvmlift3lem2  30556  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  cvmlift3  30564  mclsppslem  30734  dfon2lem1  30932  dfon2lem3  30934  dfon2lem7  30938  frrlem1  31024  nodense  31088  brofs  31282  ofscom  31284  btwnouttr  31301  brifs  31320  cgr3com  31330  brcolinear  31336  brfs  31356  unblimceq0lem  31667  knoppndvlem21  31693  csbwrecsg  32349  rdgeqoa  32394  poimirlem4  32583  poimirlem27  32606  mblfinlem3  32618  indexa  32698  sdclem1  32709  fdc  32711  neificl  32719  heiborlem2  32781  isass  32815  ismndo2  32843  isrngo  32866  rngomndo  32904  isgrpda  32924  igenval2  33035  lshpset2N  33424  isopos  33485  oposlem  33487  cmtfvalN  33515  cvrfval  33573  3dimlem1  33762  3dim1lem5  33770  lplni2  33841  lvoli2  33885  4atlem11  33913  dalawlem15  34189  cdlemftr3  34871  tendofset  35064  tendoset  35065  istendo  35066  cdlemk28-3  35214  cdlemkid3N  35239  cdlemkid4  35240  lpolsetN  35789  islpolN  35790  lpolconN  35794  ismrc  36282  rabren3dioph  36397  irrapxlem5  36408  rmydioph  36599  mpaaeu  36739  mpaaval  36740  mpaalem  36741  dfrtrcl3  37044  brco3f1o  37351  eliooshift  38576  stoweidlem5  38898  stoweidlem18  38911  stoweidlem28  38921  stoweidlem31  38924  stoweidlem41  38934  stoweidlem43  38936  stoweidlem44  38937  stoweidlem45  38938  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  issal  39210  proththdlem  40068  6gbe  40193  8gbe  40195  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  issubgr  40495  nb3grpr  40610  nb3grpr2  40611  cplgr3v  40657  1wlksfval  40811  wlksfval  40812  is1wlk  40813  isWlk  40814  upgr2wlk  40876  1wlkiswwlks2  41072  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextbij  41108  wwlksnextprop  41118  21wlkdlem4  41135  umgr2wlk  41156  umgrwwlks2on  41161  elwspths2spth  41171  isclwwlks  41188  clwlkclwwlklem1  41208  erclwwlkseq  41239  erclwwlksneq  41251  31wlkdlem5  41330  31wlkdlem6  41332  31wlkdlem9  41335  31wlkdlem10  41336  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  frgr3v  41445  3cyclfrgrrn1  41455  av-numclwlk1lem2foa  41521  el0ldep  42049  ldepspr  42056  lmod1  42075  zlmodzxzldep  42087
  Copyright terms: Public domain W3C validator