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  3401  difin2  4242  resopab2  5995  ordtri3  6353  onunel  6424  resoprab2  7479  naddsuc2  8630  psgnran  19481  efgcpbllemb  19721  cndis  23266  cnindis  23267  cnpdis  23268  blpnf  24372  dscopn  24548  itgcn  25822  limcnlp  25855  2sqreultlem  27424  2sqreunnltlem  27427  dfcgrg2  28945  nb3gr2nb  29467  uspgr2wlkeq  29729  upgrspthswlk  29821  wspthsnwspthsnon  29999  wpthswwlks2on  30047  1stpreima  32795  cntzsnid  33156  erler  33341  subsdrg  33374  qusxpid  33438  qsfld  33573  ressply1mon1p  33643  fsumcvg4  34110  mbfmcnt  34428  satfv0  35556  topdifinffinlem  37677  phpreu  37939  ptrest  37954  rngosn3  38259  isidlc  38350  dih1  41746  redvmptabs  42806  prjsperref  43053  lzunuz  43214  nadd1suc  43838  fsovrfovd  44454  uneqsn  44470  itsclquadeu  49265  pm4.71da  49277  i0oii  49407  io1ii  49408