Theorem pm4.71d 561

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.71rd  562  rabeqcda  3406  difin2  4246  resopab2  5980  ordtri3  6337  onunel  6408  resoprab2  7460  naddsuc2  8611  psgnran  19422  efgcpbllemb  19662  cndis  23201  cnindis  23202  cnpdis  23203  blpnf  24307  dscopn  24483  itgcn  25768  limcnlp  25801  2sqreultlem  27380  2sqreunnltlem  27383  dfcgrg2  28836  nb3gr2nb  29357  uspgr2wlkeq  29619  upgrspthswlk  29711  wspthsnwspthsnon  29889  wpthswwlks2on  29934  1stpreima  32680  cntzsnid  33041  erler  33224  subsdrg  33256  qusxpid  33320  qsfld  33455  ressply1mon1p  33523  fsumcvg4  33955  mbfmcnt  34273  satfv0  35394  topdifinffinlem  37381  phpreu  37644  ptrest  37659  rngosn3  37964  isidlc  38055  dih1  41325  redvmptabs  42393  prjsperref  42639  lzunuz  42801  nadd1suc  43425  fsovrfovd  44042  uneqsn  44058  itsclquadeu  48809  pm4.71da  48821  i0oii  48951  io1ii  48952