MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi123d Structured version   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  1738  sbc3ang  3211  limeq  4585  epne3  4753  smoeq  6604  ereq1  6904  indexfi  7406  hartogslem1  7501  tz9.1  7655  alephval3  7981  cofsmo  8139  cfsmolem  8140  alephsing  8146  axdc3lem2  8321  axdc3lem3  8322  axdc3  8324  axdc4lem  8325  zornn0g  8375  fpwwe2lem5  8499  canthwelem  8515  canthwe  8516  pwfseqlem4a  8526  pwfseqlem4  8527  elwina  8551  elina  8552  iswun  8569  elgrug  8657  iccshftr  11020  iccshftl  11022  iccdil  11024  icccntr  11026  fzaddel  11077  axdc4uzlem  11311  sqrmo  12047  resqrcl  12049  resqrthlem  12050  sqrneg  12063  sqreu  12154  sqrthlem  12156  eqsqrd  12161  divalglem10  12912  pythagtriplem18  13196  pythagtriplem19  13197  isstruct2  13468  imasval  13727  mreexexlemd  13859  catidd  13895  iscatd2  13896  subsubc  14040  isfunc  14051  funcres2b  14084  ispos  14394  posi  14397  isposd  14402  pospropd  14551  isps  14624  imasmnd2  14722  imasgrp2  14923  isrngd  15688  imasrng  15715  isdrngd  15850  islmod  15944  lmodlema  15945  islmodd  15946  lmodprop2d  15996  lmhmpropd  16135  assapropd  16376  isphl  16849  isphld  16875  phlpropd  16876  fiinopn  16964  iscldtop  17149  lmfval  17286  consuba  17473  1stcfb  17498  2ndcctbss  17508  subislly  17534  ptval  17592  elpt  17594  elptr  17595  upxp  17645  isfbas  17851  ustval  18222  isust  18223  ustincl  18227  ustdiag  18228  ustinvel  18229  ustexhalf  18230  ust0  18239  imasdsf1olem  18393  lmhmclm  19101  iscph  19123  iscau2  19220  pmltpclem1  19335  isi1f  19556  mbfi1fseqlem6  19602  iblcnlem  19670  dvfsumlem4  19903  aannenlem1  20235  aannenlem2  20236  ulmval  20286  nb3grapr  21452  nb3grapr2  21453  cusgra3v  21463  wlks  21516  iswlk  21517  iswlkon  21521  istrl  21527  wlkntrl  21552  is2wlk  21555  ispth  21558  2pthoncl  21593  3v3e3cycl1  21621  constr3trllem5  21631  constr3cyclpe  21640  4cycl4dv4e  21645  iseupa  21677  eupa0  21686  eupares  21687  eupap1  21688  isplig  21755  lpni  21757  isgrpo  21774  isgrpda  21875  isass  21894  ismndo2  21923  isrngo  21956  rngomndo  21999  vci  22017  isvclem  22046  isnvlem  22079  sspval  22212  isssp  22213  ajfval  22300  dipdir  22333  siilem2  22343  issh  22700  elunop2  23506  superpos  23847  resspos  24177  zhmnrg  24341  issiga  24484  isrnsigaOLD  24485  isrnsiga  24486  ismeas  24543  isrnmeas  24544  cvmlift3lem2  24997  cvmlift3lem6  25001  cvmlift3lem7  25002  cvmlift3lem9  25004  cvmlift3  25005  dfrtrcl2  25138  prodeq1f  25224  zprod  25253  dfon2lem1  25398  dfon2lem3  25400  dfon2lem7  25404  wfrlem1  25523  wfrlem15  25537  frrlem1  25547  nodense  25609  brbtwn  25803  axpaschlem  25844  axlowdim  25865  axeuclid  25867  brofs  25904  ofscom  25906  btwnouttr  25923  brifs  25942  cgr3com  25952  brcolinear  25958  brfs  25978  mblfinlem2  26208  indexa  26389  sdclem1  26401  fdc  26403  neificl  26413  heiborlem2  26475  igenval2  26630  ismrc  26709  rabren3dioph  26830  irrapxlem5  26843  rmydioph  27039  mpaaeu  27287  mpaaval  27288  mpaalem  27289  psgnunilem3  27351  stoweidlem5  27685  stoweidlem18  27698  stoweidlem28  27708  stoweidlem31  27711  stoweidlem41  27721  stoweidlem43  27723  stoweidlem44  27724  stoweidlem45  27725  stoweidlem51  27731  stoweidlem55  27735  stoweidlem59  27739  oteqimp  28017  f13dfv  28031  elfzomelpfzo  28076  usgra2pthspth  28222  usg2wlk  28236  el2wlkonot  28253  el2spthonot  28254  el2spthonot0  28255  frgra3v  28293  3cyclfrgrarn1  28303  2spotdisj  28351  bnj919  29037  bnj976  29049  bnj607  29188  bnj873  29196  lshpset2N  29818  isopos  29879  oposlem  29882  cmtfvalN  29909  cvrfval  29967  3dimlem1  30156  3dim1lem5  30164  lplni2  30235  lvoli2  30279  4atlem11  30307  dalawlem15  30583  cdlemftr3  31263  tendofset  31456  tendoset  31457  istendo  31458  cdlemk28-3  31606  cdlemkid3N  31631  cdlemkid4  31632  lpolsetN  32181  islpolN  32182  lpolconN  32186
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