Theorem pm4.71d 571

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm4.71rd  572  pm4.71da  573  rabeqcda  3423  difin2  4247  resopab2  6032  ordtri3  6394  onunel  6465  resoprab2  7532  naddsuc2  8690  qusxpid  19308  psgnran  19642  efgcpbllemb  19882  cndis  23516  cnindis  23517  cnpdis  23518  blpnf  24623  dscopn  24799  itgcn  26072  limcnlp  26105  2sqreultlem  27683  2sqreunnltlem  27686  dfcgrg2  29287  nb3gr2nb  29844  uspgr2wlkeq  30105  upgrspthswlk  30203  wspthsnwspthsnon  30384  wpthswwlks2on  30432  1stpreima  33179  cntzsnid  33520  isunitc  33681  erler  33705  subsdrg  33739  qsfld  33900  ressply1mon1p  33978  fsumcvg4  34460  mbfmcnt  34779  satfv0  35937  topdifinffinlem  38101  phpreu  38358  ptrest  38368  rngosn3  38674  isidlc  38765  dih1  42159  redvmptabs  43235  prjsperref  43452  lzunuz  43613  nadd1suc  44233  fsovrfovd  44849  uneqsn  44865  itsclquadeu  49707  i0oii  49846  io1ii  49847