Theorem pm4.71ri 700

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 698	. 2 |- ((ph -> ps) <-> (ph <-> (ps /\ ph)))
3	1, 2	mpbi 206	1 |- (ph <-> (ps /\ ph))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  sb6 1644  2moswap 1848  onzslOLD 3929  dfom2 3951  asymref 4308  asymrefOLD 4309  asymref2OLD 4311  elxp4 4379  elxp5 4380  dffun9 4450  funcnv 4475  funcnv3 4476  dff1o3OLD 4642  dff1o5OLD 4647  eufnfv 4771  abexex 4849  dff1o6 4853  dfoprab4s 5056  dfrdg2 5141  elixp2 5408  xpsnen 5494  abfii2 5652  iscard 6005  iscard2 6006  cardval2 6007  isinfcard 6035  elznn0nn 7357  zrevaddcl 7379  elnn0nn 7380  elnnnn0 7381  qrevaddcl 7455  snunioolem 7583  eluz 7595  climreu 8361  isumcl 8470  infmap2 8850  tgval2 8887  bastop2 8913  ismet 9075  isgrp 9321  isph 9822  subsp 10244  ismgm 10367  bra11 11679  mdsl2i 11894  cvmdi 11896  bnj580 13301  bnj1049 13394  bnj1070 13401  isprm3 13776  dff1o6f 14416  islatalg 14531  biadan2 15648  eroprlem 15732  fsumltisum 15824  fsumleisum 15827  prtlem100 16244

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 164  df-an 242

Copyright terms: Public domain