Theorem 3anbi23d 1300

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

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

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 369  df-3an 973

This theorem is referenced by:  f1dom3el3dif  6151  oeeui  7243  fpwwe2lem5  9001  pwfseqlem4a  9028  pwfseqlem4  9029  swrdccatin12lem3  12706  prodeq2w  13801  prodeq2ii  13802  divalg  14145  iscatd2  15170  posi  15778  issubg3  16418  pmtrfrn  16682  psgnunilem2  16719  psgnunilem3  16720  lmhmpropd  17914  lbsacsbs  17997  frlmphl  18983  neiptoptop  19799  neiptopnei  19800  cnhaus  20022  nrmsep  20025  dishaus  20050  ordthauslem  20051  nconsubb  20090  pthaus  20305  txhaus  20314  xkohaus  20320  regr1lem  20406  isust  20872  ustuqtop4  20913  methaus  21189  metnrmlem3  21531  iscau4  21884  pmltpclem1  22026  dvfsumlem2  22594  aannenlem1  22890  aannenlem2  22891  istrkgcb  24051  hlbtwn  24196  f1otrge  24377  axlowdim  24466  axeuclidlem  24467  eengtrkg  24490  wlkelwrd  24732  wlkon  24735  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv4e  24870  clwlkfclwwlk  25046  numclwwlk5  25314  ex-opab  25355  vci  25639  isvclem  25668  isnvlem  25701  dipass  25958  adj1  27050  adjeq  27052  cnlnssadj  27197  br8d  27678  carsgmon  28522  carsgsigalem  28523  carsgclctunlem2  28527  carsgclctun  28529  br8  29426  br6  29427  br4  29428  wrecseq123  29577  fvtransport  29910  brcgr3  29924  brfs  29957  fscgr  29958  btwnconn1lem11  29975  brsegle  29986  fvray  30019  linedegen  30021  fvline  30022  heiborlem2  30548  ismrc  30873  monotoddzzfi  31117  oddcomabszz  31119  zindbi  31121  rmydioph  31195  sumnnodd  31875  stoweidlem31  32052  stoweidlem34  32055  stoweidlem43  32064  stoweidlem48  32069  fourierdlem42  32170  bnj1154  34456  hlsuprexch  35502  3dim1lem5  35587  lplni2  35658  2llnjN  35688  lvoli2  35702  2lplnj  35741  cdleme18d  36417  cdlemg1cex  36711