Theorem 3anbi23d 1338

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 240	. 2 |- ( ph -> ( et <-> et ) )
2		3anbi12d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3		3anbi12d.2	. 2 |- ( ph -> ( th <-> ta ) )
4	1, 2, 3	3anbi123d 1335	1 |- ( ph -> ( ( et /\ ps /\ th ) <-> ( et /\ ch /\ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  f1dom3el3dif  6128  wrecseq123  6984  oeeui  7258  fpwwe2lem5  9010  pwfseqlem4a  9037  pwfseqlem4  9038  swrdccatin12lem3  12792  prodeq2w  13909  prodeq2ii  13910  divalg  14327  iscatd2  15530  posi  16138  issubg3  16778  pmtrfrn  17042  psgnunilem2  17079  psgnunilem3  17080  lmhmpropd  18239  lbsacsbs  18322  frlmphl  19281  neiptoptop  20089  neiptopnei  20090  cnhaus  20312  nrmsep  20315  dishaus  20340  ordthauslem  20341  nconsubb  20380  pthaus  20595  txhaus  20604  xkohaus  20610  regr1lem  20696  isust  21160  ustuqtop4  21201  methaus  21477  metnrmlem3  21820  metnrmlem3OLD  21835  iscau4  22191  pmltpclem1  22341  dvfsumlem2  22921  aannenlem1  23226  aannenlem2  23227  istrkgcb  24446  hlbtwn  24598  iscgra  24793  dfcgra2  24813  f1otrge  24844  axlowdim  24933  axeuclidlem  24934  eengtrkg  24957  wlkelwrd  25200  wlkon  25203  3v3e3cycl1  25314  4cycl4v4e  25336  4cycl4dv4e  25338  clwlkfclwwlk  25514  numclwwlk5  25782  ex-opab  25824  vci  26109  isvclem  26138  isnvlem  26171  dipass  26428  adj1  27528  adjeq  27530  cnlnssadj  27675  br8d  28164  carsgmon  29098  carsgsigalem  29099  carsgclctunlem2  29103  carsgclctun  29105  bnj1154  29760  br8  30347  br6  30348  br4  30349  fvtransport  30748  brcgr3  30762  brfs  30795  fscgr  30796  btwnconn1lem11  30813  brsegle  30824  fvray  30857  linedegen  30859  fvline  30860  poimirlem28  31875  poimirlem32  31879  heiborlem2  32051  hlsuprexch  32858  3dim1lem5  32943  lplni2  33014  2llnjN  33044  lvoli2  33058  2lplnj  33097  cdleme18d  33773  cdlemg1cex  34067  ismrc  35455  monotoddzzfi  35703  oddcomabszz  35705  zindbi  35707  rmydioph  35782  fsumiunss  37538  sumnnodd  37593  stoweidlem31  37775  stoweidlem34  37778  stoweidlem43  37787  stoweidlem48  37792  fourierdlem42  37895  fourierdlem42OLD  37896  sge0iunmptlemre  38108  sge0iunmpt  38111