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

Theorem 3anbi123d 1390
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 742 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 742 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1032 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1032 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 301 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3anbi12d  1391  3anbi13d  1392  3anbi23d  1393  ax12wdemo  1997  limeq  5634  f13dfv  6404  epne3  6845  oteqimp  7051  wfrlem1  7274  wfrlem15  7289  smoeq  7307  ereq1  7609  indexfi  8130  hartogslem1  8303  tz9.1  8461  alephval3  8789  cofsmo  8947  cfsmolem  8948  alephsing  8954  axdc3lem2  9129  axdc3lem3  9130  axdc3  9132  axdc4lem  9133  zornn0g  9183  fpwwe2lem5  9308  canthwelem  9324  canthwe  9325  pwfseqlem4a  9335  pwfseqlem4  9336  elwina  9360  elina  9361  iswun  9378  elgrug  9466  iccshftr  12129  iccshftl  12131  iccdil  12133  icccntr  12135  fzaddel  12197  elfzomelpfzo  12389  axdc4uzlem  12595  wrdl1s1  13189  wwlktovf  13489  wwlktovf1  13490  wwlktovfo  13491  wrd2f1tovbij  13493  dfrtrcl2  13592  sqrmo  13782  resqrtcl  13784  resqrtthlem  13785  sqrtneg  13798  sqreu  13890  sqrtthlem  13892  eqsqrtd  13897  prodeq1f  14419  zprod  14448  divalglem10  14905  dfgcd2  15043  coprmprod  15155  pythagtriplem18  15317  pythagtriplem19  15318  prmgaplem3  15537  prmgaplem4  15538  isstruct2  15646  imasval  15936  mreexexlemd  16069  catidd  16106  iscatd2  16107  subsubc  16278  isfunc  16289  funcres2b  16322  ispos  16712  posi  16715  isposd  16720  pospropd  16899  isps  16967  imasmnd2  17092  sgrp2rid2ex  17179  imasgrp2  17295  psgnunilem3  17681  isringd  18350  imasring  18384  isdrngd  18537  islmod  18632  lmodlema  18633  islmodd  18634  lmodprop2d  18690  lmhmpropd  18836  assapropd  19090  isphl  19733  isphld  19759  phlpropd  19760  mdetunilem3  20177  mdetunilem9  20183  fiinopn  20469  iscldtop  20647  lmfval  20784  consuba  20971  1stcfb  20996  2ndcctbss  21006  subislly  21032  ptval  21121  elpt  21123  elptr  21124  upxp  21174  isfbas  21381  ustval  21754  isust  21755  ustincl  21759  ustdiag  21760  ustinvel  21761  ustexhalf  21762  ust0  21771  imasdsf1olem  21925  lmhmclm  22622  iscph  22698  iscau2  22797  pmltpclem1  22937  isi1f  23160  mbfi1fseqlem6  23206  iblcnlem  23274  dvfsumlem4  23509  aannenlem1  23800  aannenlem2  23801  ulmval  23851  istrkgb  25067  istrkge  25069  istrkgld  25071  istrkg2ld  25072  istrkg3ld  25073  axtgupdim2  25083  axtgeucl  25084  trgcgrg  25124  ishlg  25211  colline  25258  iscgra  25415  isinag  25443  brbtwn  25493  axpaschlem  25534  axlowdim  25555  axeuclid  25557  eengtrkge  25580  nb3grapr  25744  nb3grapr2  25745  cusgra3v  25755  wlks  25809  iswlk  25810  wlkcompim  25816  wlkelwrd  25820  iswlkon  25824  istrl  25829  wlkntrl  25854  is2wlk  25857  ispth  25860  2pthoncl  25895  usg2wlk  25907  3v3e3cycl1  25934  constr3trllem5  25944  constr3cyclpe  25953  4cycl4dv4e  25958  wlkiswwlk2  25987  wwlkextfun  26019  wwlkextinj  26020  wwlkextbij  26023  wwlkextprop  26034  clwlkisclwwlklem2  26076  erclwwlkeq  26101  erclwwlkneq  26113  el2wlkonot  26158  el2spthonot  26159  el2spthonot0  26160  iseupa  26254  eupa0  26263  eupares  26264  eupap1  26265  frgra3v  26291  3cyclfrgrarn1  26301  2spotdisj  26350  numclwlk1lem2foa  26380  isplig  26482  lpni  26484  isgrpo  26497  vciOLD  26565  isvclem  26594  isnvlem  26629  sspval  26762  isssp  26763  ajfval  26850  dipdir  26883  siilem2  26893  issh  27251  elunop2  28058  superpos  28399  padct  28687  resspos  28792  isslmd  28888  slmdlema  28889  locfinreflem  29037  locfinref  29038  zhmnrg  29141  ismntoplly  29199  issiga  29303  isrnsigaOLD  29304  isrnsiga  29305  isldsys  29348  rossros  29372  ismeas  29391  isrnmeas  29392  pmeasmono  29515  pmeasadd  29516  istrkg2d  29799  axtgupdim2OLD  29801  afsval  29804  brafs  29805  bnj919  29893  bnj976  29904  bnj607  30042  bnj873  30050  cvmlift3lem2  30358  cvmlift3lem6  30362  cvmlift3lem7  30363  cvmlift3lem9  30365  cvmlift3  30366  mclsppslem  30536  dfon2lem1  30734  dfon2lem3  30736  dfon2lem7  30740  frrlem1  30826  nodense  30890  brofs  31084  ofscom  31086  btwnouttr  31103  brifs  31122  cgr3com  31132  brcolinear  31138  brfs  31158  unblimceq0lem  31469  knoppndvlem21  31495  csbwrecsg  32148  rdgeqoa  32193  poimirlem4  32382  poimirlem27  32405  mblfinlem3  32417  indexa  32497  sdclem1  32508  fdc  32510  neificl  32518  heiborlem2  32580  isass  32614  ismndo2  32642  isrngo  32665  rngomndo  32703  isgrpda  32723  igenval2  32834  lshpset2N  33223  isopos  33284  oposlem  33286  cmtfvalN  33314  cvrfval  33372  3dimlem1  33561  3dim1lem5  33569  lplni2  33640  lvoli2  33684  4atlem11  33712  dalawlem15  33988  cdlemftr3  34670  tendofset  34863  tendoset  34864  istendo  34865  cdlemk28-3  35013  cdlemkid3N  35038  cdlemkid4  35039  lpolsetN  35588  islpolN  35589  lpolconN  35593  ismrc  36081  rabren3dioph  36196  irrapxlem5  36207  rmydioph  36398  mpaaeu  36538  mpaaval  36539  mpaalem  36540  dfrtrcl3  36843  brco3f1o  37150  eliooshift  38376  stoweidlem5  38698  stoweidlem18  38711  stoweidlem28  38721  stoweidlem31  38724  stoweidlem41  38734  stoweidlem43  38736  stoweidlem44  38737  stoweidlem45  38738  stoweidlem51  38744  stoweidlem55  38748  stoweidlem59  38752  issal  39010  proththdlem  39869  6gbe  39994  8gbe  39996  bgoldbtbndlem2  40023  bgoldbtbndlem3  40024  bgoldbtbnd  40026  structvtxvallem  40251  issubgr  40493  nb3grpr  40608  nb3grpr2  40609  cplgr3v  40655  1wlksfval  40809  wlksfval  40810  is1wlk  40811  isWlk  40812  upgr2wlk  40874  1wlkiswwlks2  41070  wwlksnextfun  41102  wwlksnextinj  41103  wwlksnextbij  41106  wwlksnextprop  41116  21wlkdlem4  41133  umgr2wlk  41154  umgrwwlks2on  41159  elwspths2spth  41169  isclwwlks  41186  clwlkclwwlklem1  41206  erclwwlkseq  41237  erclwwlksneq  41249  31wlkdlem5  41328  31wlkdlem6  41330  31wlkdlem9  41333  31wlkdlem10  41334  uhgr3cyclex  41347  upgr4cycl4dv4e  41350  frgr3v  41443  3cyclfrgrrn1  41453  av-numclwlk1lem2foa  41519  el0ldep  42047  ldepspr  42054  lmod1  42073  zlmodzxzldep  42085
  Copyright terms: Public domain W3C validator