Theorem 3anbi23d 1285

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses

Ref	Expression
3anbi12d.1	|- ( ph -> ( ps <-> ch ) )
3anbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
3anbi23d	|- ( ph -> ( ( et /\ ps /\ th ) <-> ( et /\ ch /\ ta ) ) )

Proof of Theorem 3anbi23d

Step	Hyp	Ref	Expression
1		biidd 237	. 2 |- ( ph -> ( et <-> et ) )
2		3anbi12d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3		3anbi12d.2	. 2 |- ( ph -> ( th <-> ta ) )
4	1, 2, 3	3anbi123d 1282	1 |- ( ph -> ( ( et /\ ps /\ th ) <-> ( et /\ ch /\ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 958

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 960

This theorem is referenced by:  f1dom3el3dif  5968  oeeui  7029  fpwwe2lem5  8788  pwfseqlem4a  8815  pwfseqlem4  8816  swrdccatin12lem3  12364  divalg  13589  iscatd2  14601  posi  15102  issubg3  15678  pmtrfrn  15943  psgnunilem2  15980  psgnunilem3  15981  lmhmpropd  17075  lbsacsbs  17158  frlmphl  18047  neiptoptop  18576  neiptopnei  18577  cnhaus  18799  nrmsep  18802  dishaus  18827  ordthauslem  18828  nconsubb  18868  pthaus  19052  txhaus  19061  xkohaus  19067  regr1lem  19153  isust  19619  ustuqtop4  19660  methaus  19936  metnrmlem3  20278  iscau4  20631  pmltpclem1  20773  dvfsumlem2  21340  aannenlem1  21678  aannenlem2  21679  f1otrge  22940  axlowdim  23029  axeuclidlem  23030  wlkon  23251  3v3e3cycl1  23352  4cycl4v4e  23374  4cycl4dv4e  23376  ex-opab  23461  vci  23748  isvclem  23777  isnvlem  23810  dipass  24067  adj1  25159  adjeq  25161  cnlnssadj  25306  br8d  25765  prodeq2w  27271  prodeq2ii  27272  br8  27412  br6  27413  br4  27414  wrecseq123  27564  fvtransport  27909  brcgr3  27923  brfs  27956  fscgr  27957  btwnconn1lem11  27974  brsegle  27985  fvray  28018  linedegen  28020  fvline  28021  heiborlem2  28552  ismrc  28879  monotoddzzfi  29125  oddcomabszz  29127  zindbi  29129  rmydioph  29205  stoweidlem31  29669  stoweidlem34  29672  stoweidlem43  29681  stoweidlem48  29686  wlkelwrd  30123  clwlkfclwwlk  30360  numclwwlk5  30548  bnj1154  31689  hlsuprexch  32595  3dim1lem5  32680  lplni2  32751  2llnjN  32781  lvoli2  32795  2lplnj  32834  cdleme18d  33509  cdlemg1cex  33802