Theorem bianabs 542

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 529	. 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4d 283	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ceqsrexv  3587  raltpd  4623  opelopab2a  5312  ov  7150  ovg  7169  ltprord  10298  isfull  17009  isfth  17013  axcontlem5  26437  isph  28290  cmbr  29052  cvbr  29750  mdbr  29762  dmdbr  29767  brfldext  30641  brfinext  30647  soseq  32705  sltval  32763  risc  34796