Theorem 3anbi13d 895

Description: Deduction conjoining and adding a conjunct to equivalences.

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

Syntax hints:   -> wi 3   <-> wb 146   /\ w3a 775

This theorem is referenced by:  3anbi3d 899  bcpasc2t 6968  methausi 7881  metdnsconst 7901  lmbr 7928  iscau3 7938  iscau4 7940  isnvlem 8229  nvi 8233  adjvalt 9814  adjt 9857  adjeqt 9859  cnlnssadj 10013  hmph 10524  fillsb 10560  dtt2 10618  isded 10669  dedi 10670  ismonb2 10740

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain