Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71 Structured version   Visualization version   GIF version

Theorem pm4.71 660
 Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
Assertion
Ref Expression
pm4.71 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))

Proof of Theorem pm4.71
StepHypRef Expression
1 simpl 472 . . 3 ((𝜑𝜓) → 𝜑)
21biantru 525 . 2 ((𝜑 → (𝜑𝜓)) ↔ ((𝜑 → (𝜑𝜓)) ∧ ((𝜑𝜓) → 𝜑)))
3 anclb 568 . 2 ((𝜑𝜓) ↔ (𝜑 → (𝜑𝜓)))
4 dfbi2 658 . 2 ((𝜑 ↔ (𝜑𝜓)) ↔ ((𝜑 → (𝜑𝜓)) ∧ ((𝜑𝜓) → 𝜑)))
52, 3, 43bitr4i 291 1 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196  df-an 385 This theorem is referenced by:  pm4.71r  661  pm4.71i  662  pm4.71d  664  bigolden  972  pm5.75  974  pm5.75OLD  975  exintrbiOLD  1809  rabid2  3096  dfss2  3557  disj3  3973  dmopab3  5259  mptfnf  5928  cusgrauvtxb  26024  rabid2f  28724  nanorxor  37526
 Copyright terms: Public domain W3C validator