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

Theorem 3anbi123d 1254
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 692 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 692 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 938 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 938 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 280 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anbi12d  1255  3anbi13d  1256  3anbi23d  1257  ax11wdemo  1730  sbc3ang  3164  limeq  4536  epne3  4703  smoeq  6550  ereq1  6850  indexfi  7351  hartogslem1  7446  tz9.1  7600  alephval3  7926  cofsmo  8084  cfsmolem  8085  alephsing  8091  axdc3lem2  8266  axdc3lem3  8267  axdc3  8269  axdc4lem  8270  zornn0g  8320  fpwwe2lem5  8444  canthwelem  8460  canthwe  8461  pwfseqlem4a  8471  pwfseqlem4  8472  elwina  8496  elina  8497  iswun  8514  elgrug  8602  iccshftr  10964  iccshftl  10966  iccdil  10968  icccntr  10970  fzaddel  11021  axdc4uzlem  11250  sqrmo  11986  resqrcl  11988  resqrthlem  11989  sqrneg  12002  sqreu  12093  sqrthlem  12095  eqsqrd  12100  divalglem10  12851  pythagtriplem18  13135  pythagtriplem19  13136  isstruct2  13407  imasval  13666  mreexexlemd  13798  catidd  13834  iscatd2  13835  subsubc  13979  isfunc  13990  funcres2b  14023  ispos  14333  posi  14336  isposd  14341  pospropd  14490  isps  14563  imasmnd2  14661  imasgrp2  14862  isrngd  15627  imasrng  15654  isdrngd  15789  islmod  15883  lmodlema  15884  islmodd  15885  lmodprop2d  15935  lmhmpropd  16074  assapropd  16315  isphl  16784  isphld  16810  phlpropd  16811  fiinopn  16899  iscldtop  17084  lmfval  17220  consuba  17406  1stcfb  17431  2ndcctbss  17441  subislly  17467  ptval  17525  elpt  17527  elptr  17528  upxp  17578  isfbas  17784  ustval  18155  isust  18156  ustincl  18160  ustdiag  18161  ustinvel  18162  ustexhalf  18163  ust0  18172  imasdsf1olem  18313  lmhmclm  18984  iscph  19006  iscau2  19103  pmltpclem1  19214  isi1f  19435  mbfi1fseqlem6  19481  iblcnlem  19549  dvfsumlem4  19782  aannenlem1  20114  aannenlem2  20115  ulmval  20165  nb3grapr  21330  nb3grapr2  21331  cusgra3v  21341  wlks  21392  iswlk  21393  iswlkon  21397  istrl  21403  ispth  21424  2pthoncl  21453  3v3e3cycl1  21481  constr3trllem5  21491  constr3cyclpe  21500  4cycl4dv4e  21505  iseupa  21537  eupa0  21546  eupares  21547  eupap1  21548  isplig  21615  lpni  21617  isgrpo  21634  isgrpda  21735  isass  21754  ismndo2  21783  isrngo  21816  rngomndo  21859  vci  21877  isvclem  21906  isnvlem  21939  sspval  22072  isssp  22073  ajfval  22160  dipdir  22193  siilem2  22203  issh  22560  elunop2  23366  superpos  23707  resspos  24028  zhmnrg  24154  issiga  24292  isrnsigaOLD  24293  isrnsiga  24294  ismeas  24351  isrnmeas  24352  cvmlift3lem2  24788  cvmlift3lem6  24792  cvmlift3lem7  24793  cvmlift3lem9  24795  cvmlift3  24796  dfrtrcl2  24929  prodeq1f  25015  zprod  25044  dfon2lem1  25165  dfon2lem3  25167  dfon2lem7  25171  wfrlem1  25282  wfrlem15  25296  frrlem1  25307  nodense  25369  brbtwn  25554  axpaschlem  25595  axlowdim  25616  axeuclid  25618  brofs  25655  ofscom  25657  btwnouttr  25674  brifs  25693  cgr3com  25703  brcolinear  25709  brfs  25729  bpolyval  25811  indexa  26128  sdclem1  26140  fdc  26142  neificl  26152  heiborlem2  26214  igenval2  26369  ismrc  26448  rabren3dioph  26569  irrapxlem5  26582  rmydioph  26778  mpaaeu  27026  mpaaval  27027  mpaalem  27028  psgnunilem3  27090  stoweidlem5  27424  stoweidlem18  27437  stoweidlem28  27447  stoweidlem31  27450  stoweidlem41  27460  stoweidlem43  27462  stoweidlem44  27463  stoweidlem45  27464  stoweidlem51  27470  stoweidlem55  27474  stoweidlem59  27478  frgra3v  27757  3cyclfrgrarn1  27767  bnj919  28476  bnj976  28488  bnj607  28627  bnj873  28635  lshpset2N  29236  isopos  29297  oposlem  29300  cmtfvalN  29327  cvrfval  29385  3dimlem1  29574  3dim1lem5  29582  lplni2  29653  lvoli2  29697  4atlem11  29725  dalawlem15  30001  cdlemftr3  30681  tendofset  30874  tendoset  30875  istendo  30876  cdlemk28-3  31024  cdlemkid3N  31049  cdlemkid4  31050  lpolsetN  31599  islpolN  31600  lpolconN  31604
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator