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 6964  methausi 7877  metdnsconst 7897  lmbr 7924  iscau3 7934  iscau4 7936  isnvlem 8225  nvi 8229  adjvalt 9810  adjt 9853  adjeqt 9855  cnlnssadj 10009  hmph 10507  fillsb 10531  dtt2 10571  isded 10622  dedi 10623  ismonb2 10691

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