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  3597  raltpd  4725  opelopab2a  5490  ov  7511  ovg  7532  soseq  8109  ltprord  10953  isfull  17879  isfth  17883  ltsval  27611  axcontlem5  29037  isph  30893  cmbr  31655  cvbr  32353  mdbr  32365  dmdbr  32370  brfldext  33789  brfinext  33796  risc  38307