Theorem bianabs 924

Description: Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)

Hypothesis

Ref	Expression
bianabs.1	|- ( ph -> ( ps <-> ( ph /\ ch ) ) )

Assertion

Ref	Expression
bianabs	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem bianabs

Step	Hyp	Ref	Expression
1		bianabs.1	. 2 |- ( ph -> ( ps <-> ( ph /\ ch ) ) )
2		ibar 525	. 2 |- ( ph -> ( ch <-> ( ph /\ ch ) ) )
3	1, 2	bitr4d 271	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  ceqsrexv  3336  raltpd  4315  opelopab2a  4990  ov  6780  ovg  6799  ltprord  9852  isfull  16570  isfth  16574  axcontlem5  25848  isph  27677  cmbr  28443  cvbr  29141  mdbr  29153  dmdbr  29158  soseq  31751  sltval  31800  risc  33785