Theorem 3anbi13d 1401

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

Proof of Theorem 3anbi13d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		biidd 252	. 2 |- ( ph -> ( et <-> et ) )
3		3anbi12d.2	. 2 |- ( ph -> ( th <-> ta ) )
4	1, 2, 3	3anbi123d 1399	1 |- ( ph -> ( ( ps /\ et /\ th ) <-> ( ch /\ et /\ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anbi3d  1405  ax12wdemo  2012  f1dom3el3dif  6526  wfrlem1  7414  wfrlem3a  7417  wfrlem15  7429  cofsmo  9091  axdc3lem3  9274  axdc3lem4  9275  iscatd2  16342  psgnunilem1  17913  nn0gsumfz  18380  opprsubrg  18801  lsspropd  19017  mdetunilem3  20420  mdetunilem9  20426  smadiadetr  20481  lmres  21104  cnhaus  21158  regsep2  21180  dishaus  21186  ordthauslem  21187  nconnsubb  21226  pthaus  21441  txhaus  21450  xkohaus  21456  regr1lem  21542  ustval  22006  methaus  22325  metnrmlem3  22664  pmltpclem1  23217  axtgeucl  25371  iscgrad  25703  dfcgra2  25721  f1otrge  25752  axeuclidlem  25842  umgrvad2edg  26105  elwspths2spth  26862  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  vdgn1frgrv2  27160  ex-opab  27289  isnvlem  27465  ajval  27717  adjeu  28748  adjval  28749  adj1  28792  adjeq  28794  cnlnssadj  28939  br8d  29422  lt2addrd  29516  xlt2addrd  29523  measval  30261  br8  31646  br6  31647  br4  31648  brsslt  31900  brcgr3  32153  brsegle  32215  fvray  32248  linedegen  32250  fvline  32251  poimirlem28  33437  isopos  34467  hlsuprexch  34667  2llnjN  34853  2lplnj  34906  cdlemk42  36229  zindbi  37511  jm2.27  37575  stoweidlem43  40260  fourierdlem42  40366