MPE Home 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  5246  mptfnf  5914  cusgrauvtxb  25818  rabid2f  28518  nanorxor  37320
  Copyright terms: Public domain W3C validator