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  1709  sbc3ang  3062  limeq  4420  epne3  4588  smoeq  6383  ereq1  6683  indexfi  7179  hartogslem1  7273  tz9.1  7427  alephval3  7753  cofsmo  7911  cfsmolem  7912  alephsing  7918  axdc3lem2  8093  axdc3lem3  8094  axdc3  8096  axdc4lem  8097  zornn0g  8148  fpwwe2lem5  8272  canthwelem  8288  canthwe  8289  pwfseqlem4a  8299  pwfseqlem4  8300  elwina  8324  elina  8325  iswun  8342  elgrug  8430  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  axdc4uzlem  11060  sqrmo  11753  resqrcl  11755  resqrthlem  11756  sqrneg  11769  sqreu  11860  sqrthlem  11862  eqsqrd  11867  divalglem10  12617  pythagtriplem18  12901  pythagtriplem19  12902  isstruct2  13173  imasval  13430  mreexexlemd  13562  catidd  13598  iscatd2  13599  subsubc  13743  isfunc  13754  funcres2b  13787  ispos  14097  posi  14100  isposd  14105  pospropd  14254  isps  14327  imasmnd2  14425  imasgrp2  14626  isrngd  15391  imasrng  15418  isdrngd  15553  islmod  15647  lmodlema  15648  islmodd  15649  lmodprop2d  15703  lmhmpropd  15842  assapropd  16083  isphl  16548  isphld  16574  phlpropd  16575  fiinopn  16663  iscldtop  16848  lmfval  16978  consuba  17162  1stcfb  17187  2ndcctbss  17197  subislly  17223  ptval  17281  elpt  17283  elptr  17284  upxp  17333  isfbas  17540  imasdsf1olem  17953  lmhmclm  18600  iscph  18622  iscau2  18719  pmltpclem1  18824  isi1f  19045  mbfi1fseqlem6  19091  iblcnlem  19159  dvfsumlem4  19392  aannenlem1  19724  aannenlem2  19725  ulmval  19775  isplig  20860  lpni  20862  isgrpo  20879  isgrpda  20980  isass  20999  ismndo2  21028  isrngo  21061  rngomndo  21104  vci  21120  isvclem  21149  isnvlem  21182  sspval  21315  isssp  21316  ajfval  21403  dipdir  21436  siilem2  21446  issh  21803  elunop2  22609  superpos  22950  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  measval  23544  ismeas  23545  isrnmeas  23546  cvmlift3lem2  23866  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  cvmlift3  23874  iseupa  23896  eupa0  23913  eupares  23914  eupap1  23915  dfrtrcl2  24060  cprodeq1f  24130  zprod  24160  dfon2lem1  24210  dfon2lem3  24212  dfon2lem7  24216  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  nodense  24414  brbtwn  24599  axpaschlem  24640  axlowdim  24661  axeuclid  24663  brofs  24700  ofscom  24702  btwnouttr  24719  brifs  24738  cgr3com  24748  brcolinear  24754  brfs  24774  bpolyval  24856  islatalg  25286  isprsr  25327  dupre1  25346  vecval1b  25554  vecval3b  25555  vri  25595  tcnvec  25793  isalg  25824  algi  25830  isded  25839  dedi  25840  dualcat2  25887  ishomd  25893  ismona  25912  isepia  25922  isiso  25928  isfuna  25937  isfunb  25938  isntr  25976  prismorcset  26017  prismorcset2  26021  cmp2morp  26061  bisig0  26165  tethpnc2  26174  isconcl5a  26204  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  isibg2aalem3  26218  isside0  26267  isside1  26268  bosser  26270  isibcg  26294  indexa  26515  sdclem1  26556  fdc  26558  neificl  26570  heiborlem2  26639  igenval2  26794  ismrc  26879  rabren3dioph  27001  irrapxlem5  27014  rmydioph  27210  mpaaeu  27458  mpaaval  27459  mpaalem  27460  psgnunilem3  27522  stoweidlem5  27857  stoweidlem18  27870  stoweidlem28  27880  stoweidlem31  27883  stoweidlem41  27893  stoweidlem43  27895  stoweidlem44  27896  stoweidlem45  27897  stoweidlem51  27903  stoweidlem52  27904  stoweidlem55  27907  stoweidlem59  27911  nb3grapr  28289  nb3grapr2  28290  cusgra3v  28299  wlks  28328  iswlk  28329  iswlkon  28332  istrl  28336  ispth  28354  3v3e3cycl1  28390  constr3trllem5  28400  constr3cyclpe  28409  4cycl4dv4e  28414  frgra3v  28426  3cyclfrgrarn1  28435  bnj919  29113  bnj976  29125  bnj607  29264  bnj873  29272  lshpset2N  29931  isopos  29992  oposlem  29995  cmtfvalN  30022  cvrfval  30080  3dimlem1  30269  3dim1lem5  30277  lplni2  30348  lvoli2  30392  4atlem11  30420  dalawlem15  30696  cdlemftr3  31376  tendofset  31569  tendoset  31570  istendo  31571  cdlemk28-3  31719  cdlemkid3N  31744  cdlemkid4  31745  lpolsetN  32294  islpolN  32295  lpolconN  32299
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