Theorem pm4.71rd 639

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120.

Hypothesis

Ref	Expression
pm4.71rd.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
pm4.71rd	|- (ph -> (ps <-> (ch /\ ps)))

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 |- (ph -> (ps -> ch))
2		pm4.71r 636	. 2 |- ((ps -> ch) <-> (ps <-> (ch /\ ps)))
3	1, 2	sylib 198	1 |- (ph -> (ps <-> (ch /\ ps)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  axsep2 2704  reuhyp 2905  ordsucun 3082  iss 3397  fcoi1 3645  feu 3647  fnopabfv 3758  fnrnfv 3759  dff3 3818  f1fv 3874  infm3 6054  infmsup 6068  primet 6195  elcls2 7705  cncnplem3 7776  cncnp2 7779  metcn 7889  pjeqt 9242  shselt 9278

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain