Theorem 3anbi23d 1293

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 1290	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  6089  oeeui  7150  fpwwe2lem5  8911  pwfseqlem4a  8938  pwfseqlem4  8939  swrdccatin12lem3  12498  divalg  13724  iscatd2  14737  posi  15238  issubg3  15817  pmtrfrn  16082  psgnunilem2  16119  psgnunilem3  16120  lmhmpropd  17276  lbsacsbs  17359  frlmphl  18330  neiptoptop  18866  neiptopnei  18867  cnhaus  19089  nrmsep  19092  dishaus  19117  ordthauslem  19118  nconsubb  19158  pthaus  19342  txhaus  19351  xkohaus  19357  regr1lem  19443  isust  19909  ustuqtop4  19950  methaus  20226  metnrmlem3  20568  iscau4  20921  pmltpclem1  21063  dvfsumlem2  21631  aannenlem1  21926  aannenlem2  21927  f1otrge  23269  axlowdim  23358  axeuclidlem  23359  wlkon  23580  3v3e3cycl1  23681  4cycl4v4e  23703  4cycl4dv4e  23705  ex-opab  23790  vci  24077  isvclem  24106  isnvlem  24139  dipass  24396  adj1  25488  adjeq  25490  cnlnssadj  25635  br8d  26092  prodeq2w  27568  prodeq2ii  27569  br8  27709  br6  27710  br4  27711  wrecseq123  27861  fvtransport  28206  brcgr3  28220  brfs  28253  fscgr  28254  btwnconn1lem11  28271  brsegle  28282  fvray  28315  linedegen  28317  fvline  28318  heiborlem2  28858  ismrc  29184  monotoddzzfi  29430  oddcomabszz  29432  zindbi  29434  rmydioph  29510  stoweidlem31  29973  stoweidlem34  29976  stoweidlem43  29985  stoweidlem48  29990  wlkelwrd  30427  clwlkfclwwlk  30664  numclwwlk5  30852  bnj1154  32307  hlsuprexch  33348  3dim1lem5  33433  lplni2  33504  2llnjN  33534  lvoli2  33548  2lplnj  33587  cdleme18d  34262  cdlemg1cex  34555