Theorem 3anbi3d 899

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 895	1 |- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))

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

This theorem is referenced by:  so 2864  abfii3OLD 4563  abfii4OLD 4564  mulcant 5690  subbasOLD 7644  subbas2OLD 7645  iscau3 7938  iscau4 7940  isgrp2i 8076  elo 10444  spfi 10445  spfiOLD 10446  hmeogrp 10538  efilcp 10572  efilcpOLD 10573  fisub 10576  fisubOLD 10577  rcfpfillem1 10585  rcfpfillem1OLD 10586  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598

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