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  3408  difin2  4252  resopab2  5992  ordtri3  6350  onunel  6421  resoprab2  7474  naddsuc2  8625  psgnran  19437  efgcpbllemb  19677  cndis  23216  cnindis  23217  cnpdis  23218  blpnf  24322  dscopn  24498  itgcn  25783  limcnlp  25816  2sqreultlem  27395  2sqreunnltlem  27398  dfcgrg2  28851  nb3gr2nb  29373  uspgr2wlkeq  29635  upgrspthswlk  29727  wspthsnwspthsnon  29905  wpthswwlks2on  29953  1stpreima  32699  cntzsnid  33060  erler  33243  subsdrg  33275  qusxpid  33339  qsfld  33474  ressply1mon1p  33542  fsumcvg4  33974  mbfmcnt  34292  satfv0  35413  topdifinffinlem  37402  phpreu  37654  ptrest  37669  rngosn3  37974  isidlc  38065  dih1  41395  redvmptabs  42468  prjsperref  42714  lzunuz  42875  nadd1suc  43499  fsovrfovd  44116  uneqsn  44132  itsclquadeu  48892  pm4.71da  48904  i0oii  49034  io1ii  49035