Theorem pm4.71d 570

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

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

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 401

This theorem is referenced by:  pm4.71rd  571  pm4.71da  572  rabeqcda  3427  difin2  4254  resopab2  6038  ordtri3  6397  onunel  6468  resoprab2  7529  naddsuc2  8684  qusxpid  19246  psgnran  19580  efgcpbllemb  19820  cndis  23448  cnindis  23449  cnpdis  23450  blpnf  24554  dscopn  24730  itgcn  26004  limcnlp  26037  2sqreultlem  27611  2sqreunnltlem  27614  dfcgrg2  29180  nb3gr2nb  29734  uspgr2wlkeq  29995  upgrspthswlk  30087  wspthsnwspthsnon  30265  wpthswwlks2on  30313  1stpreima  33052  cntzsnid  33400  isunitc  33561  erler  33585  subsdrg  33619  qsfld  33780  ressply1mon1p  33858  fsumcvg4  34340  mbfmcnt  34658  satfv0  35850  topdifinffinlem  37993  phpreu  38255  ptrest  38270  rngosn3  38575  isidlc  38666  dih1  42060  redvmptabs  43121  prjsperref  43338  lzunuz  43499  nadd1suc  44119  fsovrfovd  44735  uneqsn  44751  itsclquadeu  49557  i0oii  49698  io1ii  49699