New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm4.71ri GIF version

Theorem pm4.71ri 614
 Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
Hypothesis
Ref Expression
pm4.71ri.1 (φψ)
Assertion
Ref Expression
pm4.71ri (φ ↔ (ψ φ))

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2 (φψ)
2 pm4.71r 612 . 2 ((φψ) ↔ (φ ↔ (ψ φ)))
31, 2mpbi 199 1 (φ ↔ (ψ φ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  biadan2  623  anabs7  785  orabs  828  prlem2  929  sb6  2099  2moswap  2279  opkelimagekg  4271  dfpw12  4301  dfnnc2  4395  eliunxp  4821  elres  4995  imadmrn  5008  elxp4  5108  dffun9  5135  funcnv  5156  funcnv3  5157  dff1o6  5475  txpcofun  5803
 Copyright terms: Public domain W3C validator