Theorem 3anbi3d 901

Description: Deduction adding conjuncts to an equivalence.

Hypothesis

Ref	Expression
3anbi1d.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
3anbi3d	|- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		pm4.2d 171	. 2 |- (ph -> (th <-> th))
2		3anbi1d.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	3anbi13d 897	1 |- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))

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

This theorem is referenced by:  so 2870  mulcant 5702  iscau3 7935  iscau4 7937  isgrp2i 8072  elo 10439  spfi 10440  hmeogrp 10524  efilcp 10556  fisub 10558  rcfpfillem1 10563  rcfpfillem3 10565  rcfpfillem6 10568  rcfpfil 10569  ishomb 10687

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 779

Copyright terms: Public domain