Theorem pm4.71i 664

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Hypothesis

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

Assertion

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

Proof of Theorem pm4.71i

Step	Hyp	Ref	Expression
1		pm4.71i.1	. 2 |- ( ph -> ps )
2		pm4.71 662	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
3	1, 2	mpbi 220	1 |- ( ph <-> ( ph /\ ps ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pm4.24  675  pm4.45  724  anabs1  850  2eu5  2557  imadmrn  5476  dff1o2  6142  f12dfv  6529  isof1oidb  6574  isof1oopb  6575  xpsnen  8044  dom0  8088  dfac5lem2  8947  pwfseqlem4  9484  axgroth6  9650  eqreznegel  11774  xrnemnf  11951  xrnepnf  11952  elioopnf  12267  elioomnf  12268  elicopnf  12269  elxrge0  12281  isprm2  15395  efgrelexlemb  18163  opsrtoslem1  19484  tgphaus  21920  cfilucfil3  23117  ioombl1lem4  23329  vitalilem1  23376  vitalilem1OLD  23377  ellogdm  24385  nb3grpr2  26285  upgr2wlk  26564  erclwwlksref  26934  erclwwlksnref  26946  0spth  26987  0crct  26993  pjimai  29035  dfrp2  29532  eulerpartlemt0  30431  bnj1101  30855  bj-snglc  32957  icorempt2  33199  wl-cases2-dnf  33295  matunitlindf  33407  pm11.58  38590