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  3610  raltpd  4739  opelopab2a  5484  ov  7504  ovg  7525  soseq  8103  ltprord  10945  isfull  17840  isfth  17844  ltsval  27619  axcontlem5  29045  isph  30901  cmbr  31663  cvbr  32361  mdbr  32373  dmdbr  32378  brfldext  33804  brfinext  33811  risc  38189