MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi23d Unicode version

Theorem 3anbi23d 1302
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1
3anbi12d.2
Assertion
Ref Expression
3anbi23d

Proof of Theorem 3anbi23d
StepHypRef Expression
1 biidd 237 . 2
2 3anbi12d.1 . 2
3 3anbi12d.2 . 2
41, 2, 33anbi123d 1299 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  f1dom3el3dif  6176  oeeui  7270  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  swrdccatin12lem3  12715  prodeq2w  13719  prodeq2ii  13720  divalg  14061  iscatd2  15078  posi  15579  issubg3  16219  pmtrfrn  16483  psgnunilem2  16520  psgnunilem3  16521  lmhmpropd  17719  lbsacsbs  17802  frlmphl  18812  neiptoptop  19632  neiptopnei  19633  cnhaus  19855  nrmsep  19858  dishaus  19883  ordthauslem  19884  nconsubb  19924  pthaus  20139  txhaus  20148  xkohaus  20154  regr1lem  20240  isust  20706  ustuqtop4  20747  methaus  21023  metnrmlem3  21365  iscau4  21718  pmltpclem1  21860  dvfsumlem2  22428  aannenlem1  22724  aannenlem2  22725  istrkgcb  23853  hlbtwn  23995  f1otrge  24175  axlowdim  24264  axeuclidlem  24265  eengtrkg  24288  wlkelwrd  24530  wlkon  24533  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  clwlkfclwwlk  24844  numclwwlk5  25112  ex-opab  25153  vci  25441  isvclem  25470  isnvlem  25503  dipass  25760  adj1  26852  adjeq  26854  cnlnssadj  26999  br8d  27463  br8  29185  br6  29186  br4  29187  wrecseq123  29337  fvtransport  29682  brcgr3  29696  brfs  29729  fscgr  29730  btwnconn1lem11  29747  brsegle  29758  fvray  29791  linedegen  29793  fvline  29794  heiborlem2  30308  ismrc  30633  monotoddzzfi  30878  oddcomabszz  30880  zindbi  30882  rmydioph  30956  sumnnodd  31636  stoweidlem31  31813  stoweidlem34  31816  stoweidlem43  31825  stoweidlem48  31830  fourierdlem42  31931  bnj1154  34055  hlsuprexch  35105  3dim1lem5  35190  lplni2  35261  2llnjN  35291  lvoli2  35305  2lplnj  35344  cdleme18d  36020  cdlemg1cex  36314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator