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

Theorem pm4.71d 617
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 613 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ps  /\  ch ) ) )
31, 2sylib 190 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  ax12bOLD  1659  difin2  3433  resopab2  5000  fcnvres  5385  resoprab2  5904  efgcpbllemb  15060  cndis  17015  cnindis  17016  cnpdis  17017  blpnf  17950  dscopn  18092  itgcn  19193  limcnlp  19224  rngosn3  21087  vtarsuelt  25296  isidlc  26041  lzunuz  26248  dih1  30745
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator