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 196 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ 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 185  df-an 371
This theorem is referenced by:  difin2  3696  resopab2  5239  fcnvres  5672  resoprab2  6273  psgnran  16109  efgcpbllemb  16342  cndis  18997  cnindis  18998  cnpdis  18999  blpnf  20074  dscopn  20268  itgcn  21422  limcnlp  21455  nb3gra2nb  23484  rngosn3  24034  1stpreima  26121  fsumcvg4  26500  mbfmcnt  26803  ptrest  28549  isidlc  28939  lzunuz  29230  usg2wlkeq  30413  clwwlkn2  30562  dih1  35213
  Copyright terms: Public domain W3C validator