Theorem pm4.71d 564

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 560	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	sylib 220	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.71rd  565  difin2  4266  resopab2  5904  ordtri3  6227  resoprab2  7271  psgnran  18643  efgcpbllemb  18881  cndis  21899  cnindis  21900  cnpdis  21901  blpnf  23007  dscopn  23183  itgcn  24443  limcnlp  24476  2sqreultlem  26023  2sqreunnltlem  26026  dfcgrg2  26649  nb3gr2nb  27166  uspgr2wlkeq  27427  upgrspthswlk  27519  wspthsnwspthsnon  27695  wpthswwlks2on  27740  1stpreima  30442  cntzsnid  30696  qusxpid  30928  fsumcvg4  31193  mbfmcnt  31526  satfv0  32605  topdifinffinlem  34631  phpreu  34891  ptrest  34906  rngosn3  35217  isidlc  35308  dih1  38437  rabeqcda  39126  prjsperref  39276  lzunuz  39385  fsovrfovd  40375  uneqsn  40393  itsclquadeu  44784