Theorem 3anbi23d 1302

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

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

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

This theorem is referenced by:  f1dom3el3dif  6162  oeeui  7248  fpwwe2lem5  9008  pwfseqlem4a  9035  pwfseqlem4  9036  swrdccatin12lem3  12674  divalg  13916  iscatd2  14932  posi  15433  issubg3  16014  pmtrfrn  16279  psgnunilem2  16316  psgnunilem3  16317  lmhmpropd  17502  lbsacsbs  17585  frlmphl  18579  neiptoptop  19398  neiptopnei  19399  cnhaus  19621  nrmsep  19624  dishaus  19649  ordthauslem  19650  nconsubb  19690  pthaus  19874  txhaus  19883  xkohaus  19889  regr1lem  19975  isust  20441  ustuqtop4  20482  methaus  20758  metnrmlem3  21100  iscau4  21453  pmltpclem1  21595  dvfsumlem2  22163  aannenlem1  22458  aannenlem2  22459  f1otrge  23851  axlowdim  23940  axeuclidlem  23941  wlkelwrd  24206  wlkon  24209  3v3e3cycl1  24320  4cycl4v4e  24342  4cycl4dv4e  24344  clwlkfclwwlk  24520  numclwwlk5  24789  ex-opab  24830  vci  25117  isvclem  25146  isnvlem  25179  dipass  25436  adj1  26528  adjeq  26530  cnlnssadj  26675  br8d  27136  prodeq2w  28621  prodeq2ii  28622  br8  28762  br6  28763  br4  28764  wrecseq123  28914  fvtransport  29259  brcgr3  29273  brfs  29306  fscgr  29307  btwnconn1lem11  29324  brsegle  29335  fvray  29368  linedegen  29370  fvline  29371  heiborlem2  29911  ismrc  30237  monotoddzzfi  30482  oddcomabszz  30484  zindbi  30486  rmydioph  30560  sumnnodd  31172  stoweidlem31  31331  stoweidlem34  31334  stoweidlem43  31343  stoweidlem48  31348  fourierdlem42  31449  bnj1154  33134  hlsuprexch  34177  3dim1lem5  34262  lplni2  34333  2llnjN  34363  lvoli2  34377  2lplnj  34416  cdleme18d  35091  cdlemg1cex  35384