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	⊢ (φ → ψ)

Assertion

Ref	Expression
pm4.71ri	⊢ (φ ↔ (ψ ⋀ φ))

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 ⊢ (φ → ψ)
2		pm4.71r 639	. 2 ⊢ ((φ → ψ) ↔ (φ ↔ (ψ ⋀ φ)))
3	1, 2	mpbi 189	1 ⊢ (φ ↔ (ψ ⋀ φ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  sb6 1271  2moswap 1449  onzsl 3133  dfom2 3149  asymref 3455  asymref2 3456  elxp4 3469  elxp5 3470  dffun8 3557  funcnv 3573  funcnv3 3574  f1o3 3710  f1o5 3713  abexex 3889  f1ofv 3893  dfrdg2 3949  elixp2 4367  xpsnen 4454  abfii2 4577  iscard 4873  iscard2 4874  cardval2 4875  isinfcard 4907  elznn0nn 6180  zrevaddcl 6202  elnn0nn 6203  elnnnn0 6204  qrevaddcl 6277  snunioolem 6382  eluz 6394  climreui 7133  isumclti 7241  infmap2 7614  tgval2 7647  bastop2 7673  ismet 7824  isgrp 8067  isph 8506  bra11 10065  mdsl2i 10274  cvmdi 10276  subsp 10587

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