Theorem 3anbi12d 1400

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

Proof of Theorem 3anbi12d

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

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:  3anbi1d  1403  3anbi2d  1404  f1dom3el3dif  6526  fseq1m1p1  12415  dfrtrcl2  13802  imasdsval  16175  iscatd2  16342  ispos  16947  psgnunilem1  17913  ringpropd  18582  mdetunilem3  20420  mdetunilem9  20426  dvfsumlem2  23790  istrkge  25356  axtg5seg  25364  axtgeucl  25371  iscgrad  25703  axlowdim  25841  axeuclid  25843  eengtrkge  25866  umgrvad2edg  26105  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  lt2addrd  29516  xlt2addrd  29523  sigaval  30173  issgon  30186  brafs  30750  etasslt  31920  brofs  32112  funtransport  32138  fvtransport  32139  brifs  32150  ifscgr  32151  brcgr3  32153  cgr3permute3  32154  brfs  32186  btwnconn1lem11  32204  funray  32247  fvray  32248  funline  32249  fvline  32251  lpolsetN  36771  rmydioph  37581  iunrelexpmin2  38004