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

Theorem pm4.71d 634
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)
Hypothesis
Ref Expression
pm4.71rd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
pm4.71d  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ch ) ) )

Proof of Theorem pm4.71d
StepHypRef Expression
1 pm4.71rd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 pm4.71 630 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ps  /\  ch ) ) )
31, 2sylib 198 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ wa 369
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 187  df-an 371
This theorem is referenced by:  difin2  3714  resopab2  5144  fcnvres  5747  resoprab2  6382  psgnran  16866  efgcpbllemb  17099  cndis  20087  cnindis  20088  cnpdis  20089  blpnf  21194  dscopn  21388  itgcn  22543  limcnlp  22576  nb3gra2nb  24884  usg2wlkeq  25137  clwwlkn2  25204  rngosn3  25855  1stpreima  27982  fsumcvg4  28398  mbfmcnt  28729  topdifinffinlem  31277  ptrest  31433  isidlc  31707  dih1  34319  lzunuz  35075
  Copyright terms: Public domain W3C validator