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

Theorem pm4.71i 613
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 611 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
31, 2mpbi 199 1  |-  ( ph  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.24  624  pm4.45  669  anabs1  783  2eu5  2240  imadmrn  5040  dff1o2  5493  map0e  6821  xpsnen  6962  dom0  7005  dfac5lem2  7767  pwfseqlem4  8300  axgroth6  8466  eqreznegel  10319  xrnemnf  10476  xrnepnf  10477  elioopnf  10753  elioomnf  10754  elicopnf  10755  elxrge0  10763  isprm2  12782  efgrelexlemb  15075  opsrtoslem1  16241  tgphaus  17815  ioombl1lem4  18934  vitalilem1  18979  ellogdm  20002  pjimai  22772  pm11.58  27692  nb3grapr2  28290  0spth  28357  0crct  28371  0cycl  28372  bnj1101  29132
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
  Copyright terms: Public domain W3C validator