Theorem pm4.71rd 394

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem pm4.71rd

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ralss  3223  rexss  3224  reuhypd  4473  elxp4  5118  elxp5  5119  dfco2a  5131  feu  5400  funbrfv2b  5562  dffn5im  5563  eqfnfv2  5616  dff4im  5664  fmptco  5684  dff13  5771  f1od2  6238  mpoxopovel  6244  brtposg  6257  dftpos3  6265  erinxp  6611  qliftfun  6619  genpdflem  7508  ltexprlemm  7601  prime  9354  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  ismgmid  12801  eqger  13088  eqgid  13090  bastop2  13669  restopn2  13768  restdis  13769  tx1cn  13854  tx2cn  13855  imasnopn  13884  xmeter  14021