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

Theorem pm4.71 612
Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
Assertion
Ref Expression
pm4.71  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )

Proof of Theorem pm4.71
StepHypRef Expression
1 simpl 444 . . 3  |-  ( (
ph  /\  ps )  ->  ph )
21biantru 492 . 2  |-  ( (
ph  ->  ( ph  /\  ps ) )  <->  ( ( ph  ->  ( ph  /\  ps ) )  /\  (
( ph  /\  ps )  ->  ph ) ) )
3 anclb 531 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ( ph  /\  ps ) ) )
4 dfbi2 610 . 2  |-  ( (
ph 
<->  ( ph  /\  ps ) )  <->  ( ( ph  ->  ( ph  /\  ps ) )  /\  (
( ph  /\  ps )  ->  ph ) ) )
52, 3, 43bitr4i 269 1  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm4.71r  613  pm4.71i  614  pm4.71d  616  bigolden  902  pm5.75  904  exintrbi  1623  rabid2  2877  dfss2  3329  disj3  3664  dmopab3  5074  cusgrauvtxb  21497  rabid2f  23959  mptfnf  24065
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 178  df-an 361
  Copyright terms: Public domain W3C validator