Theorem pm5.74d 444

Description: Distribution of implication over biconditional (deduction rule).

Hypothesis

Ref	Expression
pm5.74d.1	⊢ (φ → (ψ → (χ ↔ θ)))

Assertion

Ref	Expression
pm5.74d	⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))

Proof of Theorem pm5.74d

Step	Hyp	Ref	Expression
1		pm5.74d.1	. 2 ⊢ (φ → (ψ → (χ ↔ θ)))
2		pm5.74 442	. 2 ⊢ ((ψ → (χ ↔ θ)) ↔ ((ψ → χ) ↔ (ψ → θ)))
3	1, 2	sylib 173	1 ⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  imbi2d 464  imbi2 473  cbvald 977  biralda 1213  elpw2g 1803  oneqmini 2272  dfom2 2374  findsg 2398  tfindsg 2402  brecop 3242  dom2d 3307  indpi 3828  suplem2pr 3956  nn1suc 4435  uzind 4603  nn0ind 4612  mdbr2 5728  dmdbr2 5733

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org