ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71i Unicode version

Theorem pm4.71i 388
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
Hypothesis
Ref Expression
pm4.71i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm4.71i  |-  ( ph  <->  (
ph  /\  ps )
)

Proof of Theorem pm4.71i
StepHypRef Expression
1 pm4.71i.1 . 2  |-  ( ph  ->  ps )
2 pm4.71 386 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
31, 2mpbi 144 1  |-  ( ph  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.24  392  anabs1  546  pm4.45  758  unidif0  4061  sucexb  4383  imadmrn  4861  dff1o2  5340  xpsnen  6683  dmaddpq  7155  dmmulpq  7156  eqreznegel  9374  xrnemnf  9532  xrnepnf  9533  elioopnf  9718  elioomnf  9719  elicopnf  9720  elxrge0  9729  isprm2  11725  bj-sucexg  13047
  Copyright terms: Public domain W3C validator