Theorem pm4.71d 666

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)

Hypothesis

Ref	Expression
pm4.71rd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71d	⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Proof of Theorem pm4.71d

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		pm4.71 662	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	sylib 208	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  difin2  3890  resopab2  5448  ordtri3  5759  fcnvres  6082  resoprab2  6757  psgnran  17935  efgcpbllemb  18168  cndis  21095  cnindis  21096  cnpdis  21097  blpnf  22202  dscopn  22378  itgcn  23609  limcnlp  23642  nb3gr2nb  26286  uspgr2wlkeq  26542  upgrspthswlk  26634  wspthsnwspthsnon  26811  wpthswwlks2on  26854  1stpreima  29484  fsumcvg4  29996  mbfmcnt  30330  topdifinffinlem  33195  phpreu  33393  ptrest  33408  rngosn3  33723  isidlc  33814  dih1  36575  lzunuz  37331  fsovrfovd  38303  uneqsn  38321