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

Theorem 3anbi123d 1252
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 691 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4anbi12d 691 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et ) 
<->  ( ( ch  /\  ta )  /\  ze )
) )
6 df-3an 936 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 936 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73bitr4g 279 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anbi12d  1253  3anbi13d  1254  3anbi23d  1255  ax11wdemo  1723  sbc3ang  3125  limeq  4486  epne3  4654  smoeq  6454  ereq1  6754  indexfi  7253  hartogslem1  7347  tz9.1  7501  alephval3  7827  cofsmo  7985  cfsmolem  7986  alephsing  7992  axdc3lem2  8167  axdc3lem3  8168  axdc3  8170  axdc4lem  8171  zornn0g  8222  fpwwe2lem5  8346  canthwelem  8362  canthwe  8363  pwfseqlem4a  8373  pwfseqlem4  8374  elwina  8398  elina  8399  iswun  8416  elgrug  8504  iccshftr  10861  iccshftl  10863  iccdil  10865  icccntr  10867  fzaddel  10918  axdc4uzlem  11136  sqrmo  11833  resqrcl  11835  resqrthlem  11836  sqrneg  11849  sqreu  11940  sqrthlem  11942  eqsqrd  11947  divalglem10  12698  pythagtriplem18  12982  pythagtriplem19  12983  isstruct2  13254  imasval  13513  mreexexlemd  13645  catidd  13681  iscatd2  13682  subsubc  13826  isfunc  13837  funcres2b  13870  ispos  14180  posi  14183  isposd  14188  pospropd  14337  isps  14410  imasmnd2  14508  imasgrp2  14709  isrngd  15474  imasrng  15501  isdrngd  15636  islmod  15730  lmodlema  15731  islmodd  15732  lmodprop2d  15786  lmhmpropd  15925  assapropd  16166  isphl  16638  isphld  16664  phlpropd  16665  fiinopn  16753  iscldtop  16938  lmfval  17068  consuba  17252  1stcfb  17277  2ndcctbss  17287  subislly  17313  ptval  17371  elpt  17373  elptr  17374  upxp  17423  isfbas  17626  imasdsf1olem  18039  lmhmclm  18688  iscph  18710  iscau2  18807  pmltpclem1  18912  isi1f  19133  mbfi1fseqlem6  19179  iblcnlem  19247  dvfsumlem4  19480  aannenlem1  19812  aannenlem2  19813  ulmval  19863  isplig  20956  lpni  20958  isgrpo  20975  isgrpda  21076  isass  21095  ismndo2  21124  isrngo  21157  rngomndo  21200  vci  21218  isvclem  21247  isnvlem  21280  sspval  21413  isssp  21414  ajfval  21501  dipdir  21534  siilem2  21544  issh  21901  elunop2  22707  superpos  23048  ustval  23508  isust  23509  ustincl  23513  ustdiag  23514  ustinvel  23515  ustexhalf  23516  ust0  23523  zhmnrg  23626  issiga  23760  isrnsigaOLD  23761  isrnsiga  23762  measval  23818  ismeas  23819  isrnmeas  23820  cvmlift3lem2  24255  cvmlift3lem6  24259  cvmlift3lem7  24260  cvmlift3lem9  24262  cvmlift3  24263  iseupa  24285  eupa0  24302  eupares  24303  eupap1  24304  dfrtrcl2  24449  prodeq1f  24535  zprod  24564  dfon2lem1  24697  dfon2lem3  24699  dfon2lem7  24703  wfrlem1  24814  wfrlem15  24828  frrlem1  24839  nodense  24901  brbtwn  25086  axpaschlem  25127  axlowdim  25148  axeuclid  25150  brofs  25187  ofscom  25189  btwnouttr  25206  brifs  25225  cgr3com  25235  brcolinear  25241  brfs  25261  bpolyval  25343  indexa  25736  sdclem1  25777  fdc  25779  neificl  25791  heiborlem2  25859  igenval2  26014  ismrc  26099  rabren3dioph  26221  irrapxlem5  26234  rmydioph  26430  mpaaeu  26678  mpaaval  26679  mpaalem  26680  psgnunilem3  26742  stoweidlem5  27077  stoweidlem18  27090  stoweidlem28  27100  stoweidlem31  27103  stoweidlem41  27113  stoweidlem43  27115  stoweidlem44  27116  stoweidlem45  27117  stoweidlem51  27123  stoweidlem52  27124  stoweidlem55  27127  stoweidlem59  27131  nb3grapr  27616  nb3grapr2  27617  cusgra3v  27627  wlks  27678  iswlk  27679  iswlkon  27683  istrl  27689  ispth  27710  2pthoncl  27739  3v3e3cycl1  27768  constr3trllem5  27778  constr3cyclpe  27787  4cycl4dv4e  27792  frgra3v  27835  3cyclfrgrarn1  27845  bnj919  28559  bnj976  28571  bnj607  28710  bnj873  28718  lshpset2N  29378  isopos  29439  oposlem  29442  cmtfvalN  29469  cvrfval  29527  3dimlem1  29716  3dim1lem5  29724  lplni2  29795  lvoli2  29839  4atlem11  29867  dalawlem15  30143  cdlemftr3  30823  tendofset  31016  tendoset  31017  istendo  31018  cdlemk28-3  31166  cdlemkid3N  31191  cdlemkid4  31192  lpolsetN  31741  islpolN  31742  lpolconN  31746
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator