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

Theorem pm4.71i 636
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 634 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
31, 2mpbi 211 1  |-  ( ph  <->  (
ph  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm4.24  647  pm4.45  692  anabs1  815  2eu5  2353  imadmrn  5189  dff1o2  5827  f12dfv  6178  xpsnen  7653  dom0  7697  dfac5lem2  8544  pwfseqlem4  9076  axgroth6  9242  eqreznegel  11238  xrnemnf  11408  xrnepnf  11409  elioopnf  11717  elioomnf  11718  elicopnf  11719  elxrge0  11728  isprm2  14592  efgrelexlemb  17328  opsrtoslem1  18635  tgphaus  21055  cfilucfil3  22174  ioombl1lem4  22388  vitalilem1  22440  ellogdm  23446  nb3grapr2  25024  is2wlk  25137  0spth  25143  0crct  25196  0cycl  25197  erclwwlkref  25383  erclwwlknref  25395  pjimai  27661  dfrp2  28185  eulerpartlemt0  29025  bnj1101  29381  bj-snglc  31309  icorempt2  31485  wl-cases2-dnf  31554  pm11.58  36381
  Copyright terms: Public domain W3C validator