Theorem bianabs 541

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

Hypothesis

Ref	Expression
bianabs.1	⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒)))

Assertion

Ref	Expression
bianabs	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem bianabs

Step	Hyp	Ref	Expression
1		bianabs.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒)))
2		ibar 528	. 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4d 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ceqsrexv  3607  raltpd  4736  opelopab2a  5481  ov  7500  ovg  7521  soseq  8099  ltprord  10939  isfull  17834  isfth  17838  sltval  27613  axcontlem5  28990  isph  30846  cmbr  31608  cvbr  32306  mdbr  32318  dmdbr  32323  brfldext  33751  brfinext  33758  risc  38126