Theorem pm4.71d 565

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm4.71rd  566  rabeqcda  3395  difin2  4192  resopab2  5889  ordtri3  6227  resoprab2  7307  psgnran  18861  efgcpbllemb  19099  cndis  22142  cnindis  22143  cnpdis  22144  blpnf  23249  dscopn  23425  itgcn  24696  limcnlp  24729  2sqreultlem  26282  2sqreunnltlem  26285  dfcgrg2  26908  nb3gr2nb  27426  uspgr2wlkeq  27687  upgrspthswlk  27779  wspthsnwspthsnon  27954  wpthswwlks2on  27999  1stpreima  30713  cntzsnid  30994  qusxpid  31227  fsumcvg4  31568  mbfmcnt  31901  satfv0  32987  onunel  33359  topdifinffinlem  35204  phpreu  35447  ptrest  35462  rngosn3  35768  isidlc  35859  dih1  38986  prjsperref  40094  lzunuz  40234  fsovrfovd  41235  uneqsn  41251  itsclquadeu  45739  pm4.71da  45751  i0oii  45829  io1ii  45830