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  1697  sbc3ang  3049  limeq  4404  epne3  4572  smoeq  6367  ereq1  6667  indexfi  7163  hartogslem1  7257  tz9.1  7411  alephval3  7737  cofsmo  7895  cfsmolem  7896  alephsing  7902  axdc3lem2  8077  axdc3lem3  8078  axdc3  8080  axdc4lem  8081  zornn0g  8132  fpwwe2lem5  8256  canthwelem  8272  canthwe  8273  pwfseqlem4a  8283  pwfseqlem4  8284  elwina  8308  elina  8309  iswun  8326  elgrug  8414  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  axdc4uzlem  11044  sqrmo  11737  resqrcl  11739  resqrthlem  11740  sqrneg  11753  sqreu  11844  sqrthlem  11846  eqsqrd  11851  divalglem10  12601  pythagtriplem18  12885  pythagtriplem19  12886  isstruct2  13157  imasval  13414  mreexexlemd  13546  catidd  13582  iscatd2  13583  subsubc  13727  isfunc  13738  funcres2b  13771  ispos  14081  posi  14084  isposd  14089  pospropd  14238  isps  14311  imasmnd2  14409  imasgrp2  14610  isrngd  15375  imasrng  15402  isdrngd  15537  islmod  15631  lmodlema  15632  islmodd  15633  lmodprop2d  15687  lmhmpropd  15826  assapropd  16067  isphl  16532  isphld  16558  phlpropd  16559  fiinopn  16647  iscldtop  16832  lmfval  16962  consuba  17146  1stcfb  17171  2ndcctbss  17181  subislly  17207  ptval  17265  elpt  17267  elptr  17268  upxp  17317  isfbas  17524  imasdsf1olem  17937  lmhmclm  18584  iscph  18606  iscau2  18703  pmltpclem1  18808  isi1f  19029  mbfi1fseqlem6  19075  iblcnlem  19143  dvfsumlem4  19376  aannenlem1  19708  aannenlem2  19709  ulmval  19759  isplig  20844  lpni  20846  isgrpo  20863  isgrpda  20964  isass  20983  ismndo2  21012  isrngo  21045  rngomndo  21088  vci  21104  isvclem  21133  isnvlem  21166  sspval  21299  isssp  21300  ajfval  21387  dipdir  21420  siilem2  21430  issh  21787  elunop2  22593  superpos  22934  issiga  23472  isrnsigaOLD  23473  isrnsiga  23474  measval  23529  ismeas  23530  isrnmeas  23531  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  iseupa  23881  eupa0  23898  eupares  23899  eupap1  23900  dfrtrcl2  24045  dfon2lem1  24139  dfon2lem3  24141  dfon2lem7  24145  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  nodense  24343  brbtwn  24527  axpaschlem  24568  axlowdim  24589  axeuclid  24591  brofs  24628  ofscom  24630  btwnouttr  24647  brifs  24666  cgr3com  24676  brcolinear  24682  brfs  24702  bpolyval  24784  islatalg  25183  isprsr  25224  dupre1  25243  vecval1b  25451  vecval3b  25452  vri  25492  tcnvec  25690  isalg  25721  algi  25727  isded  25736  dedi  25737  dualcat2  25784  ishomd  25790  ismona  25809  isepia  25819  isiso  25825  isfuna  25834  isfunb  25835  isntr  25873  prismorcset  25914  prismorcset2  25918  cmp2morp  25958  bisig0  26062  tethpnc2  26071  isconcl5a  26101  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  isibg2aalem3  26115  isside0  26164  isside1  26165  bosser  26167  isibcg  26191  indexa  26412  sdclem1  26453  fdc  26455  neificl  26467  heiborlem2  26536  igenval2  26691  ismrc  26776  rabren3dioph  26898  irrapxlem5  26911  rmydioph  27107  mpaaeu  27355  mpaaval  27356  mpaalem  27357  psgnunilem3  27419  stoweidlem5  27754  stoweidlem18  27767  stoweidlem28  27777  stoweidlem31  27780  stoweidlem41  27790  stoweidlem43  27792  stoweidlem44  27793  stoweidlem45  27794  stoweidlem51  27800  stoweidlem52  27801  stoweidlem55  27804  stoweidlem59  27808  frgra3v  28180  bnj919  28797  bnj976  28809  bnj607  28948  bnj873  28956  lshpset2N  29309  isopos  29370  oposlem  29373  cmtfvalN  29400  cvrfval  29458  3dimlem1  29647  3dim1lem5  29655  lplni2  29726  lvoli2  29770  4atlem11  29798  dalawlem15  30074  cdlemftr3  30754  tendofset  30947  tendoset  30948  istendo  30949  cdlemk28-3  31097  cdlemkid3N  31122  cdlemkid4  31123  lpolsetN  31672  islpolN  31673  lpolconN  31677
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