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  1734  sbc3ang  3183  limeq  4557  epne3  4724  smoeq  6575  ereq1  6875  indexfi  7376  hartogslem1  7471  tz9.1  7625  alephval3  7951  cofsmo  8109  cfsmolem  8110  alephsing  8116  axdc3lem2  8291  axdc3lem3  8292  axdc3  8294  axdc4lem  8295  zornn0g  8345  fpwwe2lem5  8469  canthwelem  8485  canthwe  8486  pwfseqlem4a  8496  pwfseqlem4  8497  elwina  8521  elina  8522  iswun  8539  elgrug  8627  iccshftr  10990  iccshftl  10992  iccdil  10994  icccntr  10996  fzaddel  11047  axdc4uzlem  11280  sqrmo  12016  resqrcl  12018  resqrthlem  12019  sqrneg  12032  sqreu  12123  sqrthlem  12125  eqsqrd  12130  divalglem10  12881  pythagtriplem18  13165  pythagtriplem19  13166  isstruct2  13437  imasval  13696  mreexexlemd  13828  catidd  13864  iscatd2  13865  subsubc  14009  isfunc  14020  funcres2b  14053  ispos  14363  posi  14366  isposd  14371  pospropd  14520  isps  14593  imasmnd2  14691  imasgrp2  14892  isrngd  15657  imasrng  15684  isdrngd  15819  islmod  15913  lmodlema  15914  islmodd  15915  lmodprop2d  15965  lmhmpropd  16104  assapropd  16345  isphl  16818  isphld  16844  phlpropd  16845  fiinopn  16933  iscldtop  17118  lmfval  17254  consuba  17440  1stcfb  17465  2ndcctbss  17475  subislly  17501  ptval  17559  elpt  17561  elptr  17562  upxp  17612  isfbas  17818  ustval  18189  isust  18190  ustincl  18194  ustdiag  18195  ustinvel  18196  ustexhalf  18197  ust0  18206  imasdsf1olem  18360  lmhmclm  19068  iscph  19090  iscau2  19187  pmltpclem1  19302  isi1f  19523  mbfi1fseqlem6  19569  iblcnlem  19637  dvfsumlem4  19870  aannenlem1  20202  aannenlem2  20203  ulmval  20253  nb3grapr  21419  nb3grapr2  21420  cusgra3v  21430  wlks  21483  iswlk  21484  iswlkon  21488  istrl  21494  wlkntrl  21519  is2wlk  21522  ispth  21525  2pthoncl  21560  3v3e3cycl1  21588  constr3trllem5  21598  constr3cyclpe  21607  4cycl4dv4e  21612  iseupa  21644  eupa0  21653  eupares  21654  eupap1  21655  isplig  21722  lpni  21724  isgrpo  21741  isgrpda  21842  isass  21861  ismndo2  21890  isrngo  21923  rngomndo  21966  vci  21984  isvclem  22013  isnvlem  22046  sspval  22179  isssp  22180  ajfval  22267  dipdir  22300  siilem2  22310  issh  22667  elunop2  23473  superpos  23814  resspos  24144  zhmnrg  24308  issiga  24451  isrnsigaOLD  24452  isrnsiga  24453  ismeas  24510  isrnmeas  24511  cvmlift3lem2  24964  cvmlift3lem6  24968  cvmlift3lem7  24969  cvmlift3lem9  24971  cvmlift3  24972  dfrtrcl2  25105  prodeq1f  25191  zprod  25220  dfon2lem1  25357  dfon2lem3  25359  dfon2lem7  25363  wfrlem1  25474  wfrlem15  25488  frrlem1  25499  nodense  25561  brbtwn  25746  axpaschlem  25787  axlowdim  25808  axeuclid  25810  brofs  25847  ofscom  25849  btwnouttr  25866  brifs  25885  cgr3com  25895  brcolinear  25901  brfs  25921  bpolyval  26003  mblfinlem2  26148  indexa  26329  sdclem1  26341  fdc  26343  neificl  26353  heiborlem2  26415  igenval2  26570  ismrc  26649  rabren3dioph  26770  irrapxlem5  26783  rmydioph  26979  mpaaeu  27227  mpaaval  27228  mpaalem  27229  psgnunilem3  27291  stoweidlem5  27625  stoweidlem18  27638  stoweidlem28  27648  stoweidlem31  27651  stoweidlem41  27661  stoweidlem43  27663  stoweidlem44  27664  stoweidlem45  27665  stoweidlem51  27671  stoweidlem55  27675  stoweidlem59  27679  oteqimp  27955  f13dfv  27966  elfzomelpfzo  27993  usgra2pthspth  28039  usg2wlk  28053  el2wlkonot  28070  el2spthonot  28071  el2spthonot0  28072  frgra3v  28110  3cyclfrgrarn1  28120  2spotdisj  28168  bnj919  28846  bnj976  28858  bnj607  28997  bnj873  29005  lshpset2N  29606  isopos  29667  oposlem  29670  cmtfvalN  29697  cvrfval  29755  3dimlem1  29944  3dim1lem5  29952  lplni2  30023  lvoli2  30067  4atlem11  30095  dalawlem15  30371  cdlemftr3  31051  tendofset  31244  tendoset  31245  istendo  31246  cdlemk28-3  31394  cdlemkid3N  31419  cdlemkid4  31420  lpolsetN  31969  islpolN  31970  lpolconN  31974
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