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  3424  difin2  4247  resopab2  6028  ordtri3  6398  onunel  6469  resoprab2  7537  naddsuc2  8704  qusxpid  19388  psgnran  19722  efgcpbllemb  19962  cndis  23602  cnindis  23603  cnpdis  23604  blpnf  24709  dscopn  24885  itgcn  26158  limcnlp  26191  2sqreultlem  27767  2sqreunnltlem  27770  dfcgrg2  29401  nb3gr2nb  29958  uspgr2wlkeq  30219  upgrspthswlk  30317  wspthsnwspthsnon  30498  wpthswwlks2on  30546  1stpreima  33293  cntzsnid  33634  isunitc  33795  erler  33819  subsdrg  33853  qsfld  34015  ressply1mon1p  34093  fsumcvg4  34575  mbfmcnt  34893  satfv0  36102  topdifinffinlem  38250  phpreu  38507  ptrest  38517  rngosn3  38838  isidlc  38929  dih1  42323  redvmptabs  43391  prjsperref  43614  lzunuz  43758  nadd1suc  44378  fsovrfovd  44994  uneqsn  45010  itsclquadeu  49858  i0oii  49997  io1ii  49998