Theorem pm5.74d 588

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 586	. 2 ⊢ ((ψ → (χ ↔ θ)) ↔ ((ψ → χ) ↔ (ψ → θ)))
3	1, 2	sylib 198	1 ⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  pm5.74da 589  imbi2d 615  imbi2 627  cbvald 1324  2mos 1453  rcla4dv 1885  rcla4edv 1886  oneqmini 3033  findsg 3173  tfindsg 3178  brecop 4324  dom2d 4422  indpi 5054  nn1suc 5953  uzindOLD 6243  nn0ind-raph 6249  cncfmet 7931  iscms2lem4 8018  mdbr2 10248  dmdbr2 10255  mdsl2i 10274  mdsl2bi 10275  rcla4devOLD 10456

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain