Theorem 3anbi23d 1351

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

Syntax hints:   -> wi 4   <-> wb 189   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  f1dom3el3dif  6193  wrecseq123  7054  oeeui  7328  fpwwe2lem5  9084  pwfseqlem4a  9111  pwfseqlem4  9112  swrdccatin12lem3  12882  prodeq2w  14014  prodeq2ii  14015  divalg  14432  iscatd2  15635  posi  16243  issubg3  16883  pmtrfrn  17147  psgnunilem2  17184  psgnunilem3  17185  lmhmpropd  18344  lbsacsbs  18427  frlmphl  19387  neiptoptop  20195  neiptopnei  20196  cnhaus  20418  nrmsep  20421  dishaus  20446  ordthauslem  20447  nconsubb  20486  pthaus  20701  txhaus  20710  xkohaus  20716  regr1lem  20802  isust  21266  ustuqtop4  21307  methaus  21583  metnrmlem3  21926  metnrmlem3OLD  21941  iscau4  22297  pmltpclem1  22447  dvfsumlem2  23027  aannenlem1  23332  aannenlem2  23333  istrkgcb  24552  hlbtwn  24704  iscgra  24899  dfcgra2  24919  f1otrge  24950  axlowdim  25039  axeuclidlem  25040  eengtrkg  25063  wlkelwrd  25306  wlkon  25309  3v3e3cycl1  25420  4cycl4v4e  25442  4cycl4dv4e  25444  clwlkfclwwlk  25620  numclwwlk5  25888  ex-opab  25930  vci  26215  isvclem  26244  isnvlem  26277  dipass  26534  adj1  27634  adjeq  27636  cnlnssadj  27781  br8d  28266  carsgmon  29194  carsgsigalem  29195  carsgclctunlem2  29199  carsgclctun  29201  bnj1154  29856  br8  30444  br6  30445  br4  30446  fvtransport  30847  brcgr3  30861  brfs  30894  fscgr  30895  btwnconn1lem11  30912  brsegle  30923  fvray  30956  linedegen  30958  fvline  30959  poimirlem28  32012  poimirlem32  32016  heiborlem2  32188  hlsuprexch  32990  3dim1lem5  33075  lplni2  33146  2llnjN  33176  lvoli2  33190  2lplnj  33229  cdleme18d  33905  cdlemg1cex  34199  ismrc  35587  monotoddzzfi  35834  oddcomabszz  35836  zindbi  35838  rmydioph  35913  fsumiunss  37691  sumnnodd  37747  stoweidlem31  37929  stoweidlem34  37932  stoweidlem43  37941  stoweidlem48  37946  fourierdlem42  38049  fourierdlem42OLD  38050  sge0iunmptlemre  38294  sge0iunmpt  38297  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925