Theorem 3anbi23d 1292

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 1289	1 |- ( ph -> ( ( et /\ ps /\ th ) <-> ( et /\ ch /\ ta ) ) )

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

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 967

This theorem is referenced by:  f1dom3el3dif  5976  oeeui  7033  fpwwe2lem5  8793  pwfseqlem4a  8820  pwfseqlem4  8821  swrdccatin12lem3  12373  divalg  13599  iscatd2  14611  posi  15112  issubg3  15690  pmtrfrn  15955  psgnunilem2  15992  psgnunilem3  15993  lmhmpropd  17134  lbsacsbs  17217  frlmphl  18186  neiptoptop  18715  neiptopnei  18716  cnhaus  18938  nrmsep  18941  dishaus  18966  ordthauslem  18967  nconsubb  19007  pthaus  19191  txhaus  19200  xkohaus  19206  regr1lem  19292  isust  19758  ustuqtop4  19799  methaus  20075  metnrmlem3  20417  iscau4  20770  pmltpclem1  20912  dvfsumlem2  21479  aannenlem1  21774  aannenlem2  21775  f1otrge  23086  axlowdim  23175  axeuclidlem  23176  wlkon  23397  3v3e3cycl1  23498  4cycl4v4e  23520  4cycl4dv4e  23522  ex-opab  23607  vci  23894  isvclem  23923  isnvlem  23956  dipass  24213  adj1  25305  adjeq  25307  cnlnssadj  25452  br8d  25910  prodeq2w  27394  prodeq2ii  27395  br8  27535  br6  27536  br4  27537  wrecseq123  27687  fvtransport  28032  brcgr3  28046  brfs  28079  fscgr  28080  btwnconn1lem11  28097  brsegle  28108  fvray  28141  linedegen  28143  fvline  28144  heiborlem2  28682  ismrc  29008  monotoddzzfi  29254  oddcomabszz  29256  zindbi  29258  rmydioph  29334  stoweidlem31  29797  stoweidlem34  29800  stoweidlem43  29809  stoweidlem48  29814  wlkelwrd  30251  clwlkfclwwlk  30488  numclwwlk5  30676  bnj1154  31919  hlsuprexch  32918  3dim1lem5  33003  lplni2  33074  2llnjN  33104  lvoli2  33118  2lplnj  33157  cdleme18d  33832  cdlemg1cex  34125