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  3427  difin2  4249  resopab2  6046  ordtri3  6425  onunel  6496  resoprab2  7570  naddsuc2  8749  qusxpid  19445  psgnran  19780  efgcpbllemb  20020  cndis  23664  cnindis  23665  cnpdis  23666  blpnf  24771  dscopn  24947  itgcn  26220  limcnlp  26253  2sqreultlem  27831  2sqreunnltlem  27834  dfcgrg2  29465  nb3gr2nb  30022  uspgr2wlkeq  30283  upgrspthswlk  30381  wspthsnwspthsnon  30562  wpthswwlks2on  30610  1stpreima  33397  cntzsnid  33740  isunitc  33901  erler  33925  subsdrg  33964  qsfld  34126  ressply1mon1p  34203  fsumcvg4  34693  mbfmcnt  35011  satfv0  36331  topdifinffinlem  38538  phpreu  38795  ptrest  38805  rngosn3  39124  isidlc  39215  dih1  42609  redvmptabs  43677  prjsperref  43900  lzunuz  44045  nadd1suc  44655  fsovrfovd  45270  uneqsn  45286  itsclquadeu  50220  i0oii  50365  io1ii  50366