Theorem 3anbi23d 896

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

Proof of Theorem 3anbi23d

Step	Hyp	Ref	Expression
1		pm4.2d 171	. 2 |- (ph -> (et <-> et))
2		3anbi12d.1	. 2 |- (ph -> (ps <-> ch))
3		3anbi12d.2	. 2 |- (ph -> (th <-> ta))
4	1, 2, 3	3anbi123d 893	1 |- (ph -> ((et /\ ps /\ th) <-> (et /\ ch /\ ta)))

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

This theorem is referenced by:  bcpasc2t 6968  methausi 7881  lmbr 7928  iscau3 7938  iscau4 7940  isring 8141  ringi 8142  vci 8167  isvclem 8196  isnvlem 8229  nvi 8233  ipass 8505  adjt 9857  adjeqt 9859  cnlnssadj 10013  hmph 10524  hmeobc 10542  fillsb 10560  sfvlim 10605  dtt2 10618  isalg 10653  algi 10660  ismonb 10738  isepib 10748

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