Theorem pm4.71rd 638

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 635	. 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 2699  reuhyp 2900  ordsucun 3077  iss 3389  fcoi1 3636  feu 3638  fnopabfv 3749  fnrnfv 3750  dff3 3809  f1fv 3865  infm3 6009  infmsup 6023  primet 6150  elcls2 7655  cncnplem3 7726  cncnp2 7729  metcn 7841  pjeqt 9180  shselt 9216

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