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

Theorem 3anbi123d 1255
Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi3d.2  |-  ( ph  ->  ( th  <->  ta )
)
bi3d.3  |-  ( ph  ->  ( et  <->  ze )
)
Assertion
Ref Expression
3anbi123d  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )

Proof of Theorem 3anbi123d
StepHypRef Expression
1 bi3d.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi3d.2 . . . 4  |-  ( ph  ->  ( th  <->  ta )
)
31, 2anbi12d 693 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 693 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 939 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 939 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 281 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anbi12d  1256  3anbi13d  1257  3anbi23d  1258  ax11wdemo  1740  sbc3angOLD  3229  limeq  4622  epne3  4790  smoeq  6641  ereq1  6941  indexfi  7443  hartogslem1  7540  tz9.1  7694  alephval3  8022  cofsmo  8180  cfsmolem  8181  alephsing  8187  axdc3lem2  8362  axdc3lem3  8363  axdc3  8365  axdc4lem  8366  zornn0g  8416  fpwwe2lem5  8540  canthwelem  8556  canthwe  8557  pwfseqlem4a  8567  pwfseqlem4  8568  elwina  8592  elina  8593  iswun  8610  elgrug  8698  iccshftr  11061  iccshftl  11063  iccdil  11065  icccntr  11067  fzaddel  11118  axdc4uzlem  11352  sqrmo  12088  resqrcl  12090  resqrthlem  12091  sqrneg  12104  sqreu  12195  sqrthlem  12197  eqsqrd  12202  divalglem10  12953  pythagtriplem18  13237  pythagtriplem19  13238  isstruct2  13509  imasval  13768  mreexexlemd  13900  catidd  13936  iscatd2  13937  subsubc  14081  isfunc  14092  funcres2b  14125  ispos  14435  posi  14438  isposd  14443  pospropd  14592  isps  14665  imasmnd2  14763  imasgrp2  14964  isrngd  15729  imasrng  15756  isdrngd  15891  islmod  15985  lmodlema  15986  islmodd  15987  lmodprop2d  16037  lmhmpropd  16176  assapropd  16417  isphl  16890  isphld  16916  phlpropd  16917  fiinopn  17005  iscldtop  17190  lmfval  17327  consuba  17514  1stcfb  17539  2ndcctbss  17549  subislly  17575  ptval  17633  elpt  17635  elptr  17636  upxp  17686  isfbas  17892  ustval  18263  isust  18264  ustincl  18268  ustdiag  18269  ustinvel  18270  ustexhalf  18271  ust0  18280  imasdsf1olem  18434  lmhmclm  19142  iscph  19164  iscau2  19261  pmltpclem1  19376  isi1f  19595  mbfi1fseqlem6  19641  iblcnlem  19709  dvfsumlem4  19944  aannenlem1  20276  aannenlem2  20277  ulmval  20327  nb3grapr  21493  nb3grapr2  21494  cusgra3v  21504  wlks  21557  iswlk  21558  iswlkon  21562  istrl  21568  wlkntrl  21593  is2wlk  21596  ispth  21599  2pthoncl  21634  3v3e3cycl1  21662  constr3trllem5  21672  constr3cyclpe  21681  4cycl4dv4e  21686  iseupa  21718  eupa0  21727  eupares  21728  eupap1  21729  isplig  21796  lpni  21798  isgrpo  21815  isgrpda  21916  isass  21935  ismndo2  21964  isrngo  21997  rngomndo  22040  vci  22058  isvclem  22087  isnvlem  22120  sspval  22253  isssp  22254  ajfval  22341  dipdir  22374  siilem2  22384  issh  22741  elunop2  23547  superpos  23888  resspos  24218  zhmnrg  24382  issiga  24525  isrnsigaOLD  24526  isrnsiga  24527  ismeas  24584  isrnmeas  24585  cvmlift3lem2  25038  cvmlift3lem6  25042  cvmlift3lem7  25043  cvmlift3lem9  25045  cvmlift3  25046  dfrtrcl2  25179  prodeq1f  25265  zprod  25294  dfon2lem1  25441  dfon2lem3  25443  dfon2lem7  25447  wfrlem1  25569  wfrlem15  25583  frrlem1  25613  nodense  25675  brbtwn  25869  axpaschlem  25910  axlowdim  25931  axeuclid  25933  brofs  25970  ofscom  25972  btwnouttr  25989  brifs  26008  cgr3com  26018  brcolinear  26024  brfs  26044  mblfinlem3  26281  indexa  26473  sdclem1  26485  fdc  26487  neificl  26497  heiborlem2  26559  igenval2  26714  ismrc  26793  rabren3dioph  26914  irrapxlem5  26927  rmydioph  27123  mpaaeu  27370  mpaaval  27371  mpaalem  27372  psgnunilem3  27434  stoweidlem5  27768  stoweidlem18  27781  stoweidlem28  27791  stoweidlem31  27794  stoweidlem41  27804  stoweidlem43  27806  stoweidlem44  27807  stoweidlem45  27808  stoweidlem51  27814  stoweidlem55  27818  stoweidlem59  27822  oteqimp  28102  f13dfv  28123  elfzomelpfzo  28176  wlkelwrd  28357  wlkcompim  28364  usgra2pthspth  28367  usg2wlk  28381  wlkiswwlk2  28403  el2wlkonot  28425  el2spthonot  28426  el2spthonot0  28427  frgra3v  28490  3cyclfrgrarn1  28500  2spotdisj  28548  bnj919  29234  bnj976  29246  bnj607  29385  bnj873  29393  lshpset2N  30015  isopos  30076  oposlem  30079  cmtfvalN  30106  cvrfval  30164  3dimlem1  30353  3dim1lem5  30361  lplni2  30432  lvoli2  30476  4atlem11  30504  dalawlem15  30780  cdlemftr3  31460  tendofset  31653  tendoset  31654  istendo  31655  cdlemk28-3  31803  cdlemkid3N  31828  cdlemkid4  31829  lpolsetN  32378  islpolN  32379  lpolconN  32383
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator