Theorem pm4.71ri 641

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).

Hypothesis

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

Assertion

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

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 |- (ph -> ps)
2		pm4.71r 639	. 2 |- ((ph -> ps) <-> (ph <-> (ps /\ ph)))
3	1, 2	mpbi 187	1 |- (ph <-> (ps /\ ph))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  sb6 1305  2moswap 1484  onzsl 3200  dfom2 3220  asymref 3531  asymref2 3532  elxp4 3585  elxp5 3586  dffun9 3646  funcnv 3662  funcnv3 3663  dff1o3 3802  dff1o5 3805  abexex 3987  dff1o6 3991  dfoprab4s 4176  dfrdg2 4234  elixp2 4490  xpsnen 4576  abfii2 4705  iscard 5003  iscard2 5004  cardval2 5005  isinfcard 5037  elznn0nn 6316  zrevaddcl 6338  elnn0nn 6339  elnnnn0 6340  qrevaddcl 6414  snunioolem 6541  eluz 6553  climreu 7304  isumcl 7413  infmap2 7793  tgval2 7829  bastop2 7855  ismet 8008  isgrp 8254  isph 8737  bra11 10321  mdsl2i 10530  cvmdi 10532  islatalg 10831  ismgm 10897  subsp 11056  fsumltisum 11887  fsumleisum 11890

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 145  df-an 223

Copyright terms: Public domain