Theorem pm4.71ri 636

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

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

This theorem is referenced by:  sb6 1262  2moswap 1437  onzsl 3107  dfom2 3123  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  elxp4 3439  elxp5 3440  dffun8 3527  funcnv 3543  funcnv3 3544  f1o3 3679  f1o5 3682  abexex 3858  f1ofv 3862  dfrdg2 3918  elixp2 4333  xpsnen 4415  abfii2 4536  iscard 4825  iscard2 4826  cardval2 4827  isinfcard 4859  elznn0nn 6095  zrevaddclt 6117  elnn0nn 6118  elnnnn0 6119  qrevaddclt 6213  snunioolem 6347  eluzt 6358  climreu 7038  isumclt 7144  infmap2 7523  tgval2t 7559  bastop2 7585  ismet 7737  isgrp 7975  isph 8412  bra11 9954  mdsl2 10157  cvmd 10159  subsp 10429

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