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  2227  imadmrn  5024  dff1o2  5477  map0e  6805  xpsnen  6946  dom0  6989  dfac5lem2  7751  pwfseqlem4  8284  axgroth6  8450  eqreznegel  10303  xrnemnf  10460  xrnepnf  10461  elioopnf  10737  elioomnf  10738  elicopnf  10739  elxrge0  10747  isprm2  12766  efgrelexlemb  15059  opsrtoslem1  16225  tgphaus  17799  ioombl1lem4  18918  vitalilem1  18963  ellogdm  19986  pjimai  22756  pm11.58  27589  bnj1101  28816
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