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  3760  resopab2  5320  fcnvres  5760  resoprab2  6381  psgnran  16336  efgcpbllemb  16569  cndis  19558  cnindis  19559  cnpdis  19560  blpnf  20635  dscopn  20829  itgcn  21984  limcnlp  22017  nb3gra2nb  24131  usg2wlkeq  24384  clwwlkn2  24451  rngosn3  25104  1stpreima  27196  fsumcvg4  27568  mbfmcnt  27879  ptrest  29625  isidlc  30015  lzunuz  30305  dih1  36083
  Copyright terms: Public domain W3C validator