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

Theorem 3anbi123d 1397
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 746 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 746 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1038 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1038 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 303 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036
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 1038
This theorem is referenced by:  3anbi12d  1398  3anbi13d  1399  3anbi23d  1400  ax12wdemo  2010  limeq  5723  f13dfv  6515  epne3  6965  oteqimp  7172  wfrlem1  7399  wfrlem15  7414  smoeq  7432  ereq1  7734  indexfi  8259  hartogslem1  8432  tz9.1  8590  alephval3  8918  cofsmo  9076  cfsmolem  9077  alephsing  9083  axdc3lem2  9258  axdc3lem3  9259  axdc3  9261  axdc4lem  9262  zornn0g  9312  fpwwe2lem5  9441  canthwelem  9457  canthwe  9458  pwfseqlem4a  9468  pwfseqlem4  9469  elwina  9493  elina  9494  iswun  9511  elgrug  9599  iccshftr  12291  iccshftl  12293  iccdil  12295  icccntr  12297  fzaddel  12360  elfzomelpfzo  12556  axdc4uzlem  12765  wrdl1s1  13377  wwlktovf  13680  wwlktovf1  13681  wwlktovfo  13682  wrd2f1tovbij  13684  dfrtrcl2  13783  sqrmo  13973  resqrtcl  13975  resqrtthlem  13976  sqrtneg  13989  sqreu  14081  sqrtthlem  14083  eqsqrtd  14088  prodeq1f  14619  zprod  14648  divalglem10  15106  dfgcd2  15244  coprmprod  15356  pythagtriplem18  15518  pythagtriplem19  15519  prmgaplem3  15738  prmgaplem4  15739  isstruct2  15848  imasval  16152  mreexexlemd  16285  catidd  16322  iscatd2  16323  subsubc  16494  isfunc  16505  funcres2b  16538  ispos  16928  posi  16931  isposd  16936  pospropd  17115  isps  17183  imasmnd2  17308  sgrp2rid2ex  17395  imasgrp2  17511  psgnunilem3  17897  isringd  18566  imasring  18600  isdrngd  18753  islmod  18848  lmodlema  18849  islmodd  18850  lmodprop2d  18906  lmhmpropd  19054  assapropd  19308  isphl  19954  isphld  19980  phlpropd  19981  mdetunilem3  20401  mdetunilem9  20407  fiinopn  20687  iscldtop  20880  lmfval  21017  connsuba  21204  1stcfb  21229  2ndcctbss  21239  subislly  21265  ptval  21354  elpt  21356  elptr  21357  upxp  21407  isfbas  21614  ustval  21987  isust  21988  ustincl  21992  ustdiag  21993  ustinvel  21994  ustexhalf  21995  ust0  22004  imasdsf1olem  22159  tngngp3  22441  lmhmclm  22868  iscph  22951  iscau2  23056  pmltpclem1  23198  isi1f  23422  mbfi1fseqlem6  23468  iblcnlem  23536  dvfsumlem4  23773  aannenlem1  24064  aannenlem2  24065  ulmval  24115  istrkgb  25335  istrkge  25337  istrkgld  25339  istrkg2ld  25340  istrkg3ld  25341  axtgupdim2  25351  axtgeucl  25352  trgcgrg  25391  ishlg  25478  colline  25525  iscgra  25682  isinag  25710  brbtwn  25760  axpaschlem  25801  axlowdim  25822  axeuclid  25824  eengtrkge  25847  issubgr  26144  nb3grpr  26265  nb3grpr2  26266  cplgr3v  26312  wksfval  26486  iswlk  26487  upgr2wlk  26545  wlkiswwlks2  26742  wwlksnextfun  26774  wwlksnextinj  26775  wwlksnextbij  26778  wwlksnextprop  26788  2wlkdlem4  26805  umgr2wlk  26826  umgrwwlks2on  26831  elwspths2spth  26843  isclwwlks  26861  clwlkclwwlklem1  26881  erclwwlkseq  26912  erclwwlksneq  26924  3wlkdlem5  27003  3wlkdlem6  27005  3wlkdlem9  27008  3wlkdlem10  27009  uhgr3cyclex  27022  upgr4cycl4dv4e  27025  frgr3v  27119  3cyclfrgrrn1  27129  numclwlk1lem2foa  27195  isplig  27298  lpni  27302  isgrpo  27321  vciOLD  27386  isvclem  27402  isnvlem  27435  sspval  27548  isssp  27549  ajfval  27634  dipdir  27667  siilem2  27677  issh  28035  elunop2  28842  superpos  29183  padct  29471  resspos  29633  isslmd  29729  slmdlema  29730  locfinreflem  29881  locfinref  29882  zhmnrg  29985  ismntoplly  30043  issiga  30148  isrnsigaOLD  30149  isrnsiga  30150  isldsys  30193  rossros  30217  ismeas  30236  isrnmeas  30237  pmeasmono  30360  pmeasadd  30361  istrkg2d  30718  axtgupdim2OLD  30720  afsval  30723  brafs  30724  bnj919  30811  bnj976  30822  bnj607  30960  bnj873  30968  cvmlift3lem2  31276  cvmlift3lem6  31280  cvmlift3lem7  31281  cvmlift3lem9  31283  cvmlift3  31284  mclsppslem  31454  dfon2lem1  31662  dfon2lem3  31664  dfon2lem7  31668  frrlem1  31754  nodense  31816  noprefixmo  31822  nosupfv  31826  noetalem5  31841  noeta  31842  brofs  32087  ofscom  32089  btwnouttr  32106  brifs  32125  cgr3com  32135  brcolinear  32141  brfs  32161  unblimceq0lem  32472  knoppndvlem21  32498  csbwrecsg  33144  rdgeqoa  33189  poimirlem4  33384  poimirlem27  33407  mblfinlem3  33419  indexa  33499  sdclem1  33510  fdc  33512  neificl  33520  heiborlem2  33582  isass  33616  ismndo2  33644  isrngo  33667  rngomndo  33705  isgrpda  33725  igenval2  33836  lshpset2N  34225  isopos  34286  oposlem  34288  cmtfvalN  34316  cvrfval  34374  3dimlem1  34563  3dim1lem5  34571  lplni2  34642  lvoli2  34686  4atlem11  34714  dalawlem15  34990  cdlemftr3  35672  tendofset  35865  tendoset  35866  istendo  35867  cdlemk28-3  36015  cdlemkid3N  36040  cdlemkid4  36041  lpolsetN  36590  islpolN  36591  lpolconN  36595  ismrc  37083  rabren3dioph  37198  irrapxlem5  37209  rmydioph  37400  mpaaeu  37539  mpaaval  37540  mpaalem  37541  dfrtrcl3  37844  brco3f1o  38151  eliooshift  39532  stoweidlem5  39985  stoweidlem18  39998  stoweidlem28  40008  stoweidlem31  40011  stoweidlem41  40021  stoweidlem43  40023  stoweidlem44  40024  stoweidlem45  40025  stoweidlem51  40031  stoweidlem55  40035  stoweidlem59  40039  issal  40297  proththdlem  41295  6gbe  41424  8gbe  41426  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  bgoldbtbnd  41462  upwlksfval  41481  isupwlk  41482  el0ldep  42020  ldepspr  42027  lmod1  42046  zlmodzxzldep  42058
  Copyright terms: Public domain W3C validator