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  3179  limeq  4553  epne3  4720  smoeq  6571  ereq1  6871  indexfi  7372  hartogslem1  7467  tz9.1  7621  alephval3  7947  cofsmo  8105  cfsmolem  8106  alephsing  8112  axdc3lem2  8287  axdc3lem3  8288  axdc3  8290  axdc4lem  8291  zornn0g  8341  fpwwe2lem5  8465  canthwelem  8481  canthwe  8482  pwfseqlem4a  8492  pwfseqlem4  8493  elwina  8517  elina  8518  iswun  8535  elgrug  8623  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  fzaddel  11043  axdc4uzlem  11276  sqrmo  12012  resqrcl  12014  resqrthlem  12015  sqrneg  12028  sqreu  12119  sqrthlem  12121  eqsqrd  12126  divalglem10  12877  pythagtriplem18  13161  pythagtriplem19  13162  isstruct2  13433  imasval  13692  mreexexlemd  13824  catidd  13860  iscatd2  13861  subsubc  14005  isfunc  14016  funcres2b  14049  ispos  14359  posi  14362  isposd  14367  pospropd  14516  isps  14589  imasmnd2  14687  imasgrp2  14888  isrngd  15653  imasrng  15680  isdrngd  15815  islmod  15909  lmodlema  15910  islmodd  15911  lmodprop2d  15961  lmhmpropd  16100  assapropd  16341  isphl  16814  isphld  16840  phlpropd  16841  fiinopn  16929  iscldtop  17114  lmfval  17250  consuba  17436  1stcfb  17461  2ndcctbss  17471  subislly  17497  ptval  17555  elpt  17557  elptr  17558  upxp  17608  isfbas  17814  ustval  18185  isust  18186  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  imasdsf1olem  18356  lmhmclm  19064  iscph  19086  iscau2  19183  pmltpclem1  19298  isi1f  19519  mbfi1fseqlem6  19565  iblcnlem  19633  dvfsumlem4  19866  aannenlem1  20198  aannenlem2  20199  ulmval  20249  nb3grapr  21415  nb3grapr2  21416  cusgra3v  21426  wlks  21479  iswlk  21480  iswlkon  21484  istrl  21490  wlkntrl  21515  is2wlk  21518  ispth  21521  2pthoncl  21556  3v3e3cycl1  21584  constr3trllem5  21594  constr3cyclpe  21603  4cycl4dv4e  21608  iseupa  21640  eupa0  21649  eupares  21650  eupap1  21651  isplig  21718  lpni  21720  isgrpo  21737  isgrpda  21838  isass  21857  ismndo2  21886  isrngo  21919  rngomndo  21962  vci  21980  isvclem  22009  isnvlem  22042  sspval  22175  isssp  22176  ajfval  22263  dipdir  22296  siilem2  22306  issh  22663  elunop2  23469  superpos  23810  resspos  24140  zhmnrg  24304  issiga  24447  isrnsigaOLD  24448  isrnsiga  24449  ismeas  24506  isrnmeas  24507  cvmlift3lem2  24960  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  cvmlift3  24968  dfrtrcl2  25101  prodeq1f  25187  zprod  25216  dfon2lem1  25353  dfon2lem3  25355  dfon2lem7  25359  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  nodense  25557  brbtwn  25742  axpaschlem  25783  axlowdim  25804  axeuclid  25806  brofs  25843  ofscom  25845  btwnouttr  25862  brifs  25881  cgr3com  25891  brcolinear  25897  brfs  25917  bpolyval  25999  mblfinlem2  26144  indexa  26325  sdclem1  26337  fdc  26339  neificl  26349  heiborlem2  26411  igenval2  26566  ismrc  26645  rabren3dioph  26766  irrapxlem5  26779  rmydioph  26975  mpaaeu  27223  mpaaval  27224  mpaalem  27225  psgnunilem3  27287  stoweidlem5  27621  stoweidlem18  27634  stoweidlem28  27644  stoweidlem31  27647  stoweidlem41  27657  stoweidlem43  27659  stoweidlem44  27660  stoweidlem45  27661  stoweidlem51  27667  stoweidlem55  27671  stoweidlem59  27675  oteqimp  27951  f13dfv  27962  elfzomelpfzo  27989  usgra2pthspth  28035  usg2wlk  28049  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  frgra3v  28106  3cyclfrgrarn1  28116  2spotdisj  28164  bnj919  28842  bnj976  28854  bnj607  28993  bnj873  29001  lshpset2N  29602  isopos  29663  oposlem  29666  cmtfvalN  29693  cvrfval  29751  3dimlem1  29940  3dim1lem5  29948  lplni2  30019  lvoli2  30063  4atlem11  30091  dalawlem15  30367  cdlemftr3  31047  tendofset  31240  tendoset  31241  istendo  31242  cdlemk28-3  31390  cdlemkid3N  31415  cdlemkid4  31416  lpolsetN  31965  islpolN  31966  lpolconN  31970
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