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

Theorem pm4.71d 618
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 614 . 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:  difin2  3337  resopab2  4906  fcnvres  5275  resoprab2  5793  efgcpbllemb  14899  cndis  16851  cnindis  16852  cnpdis  16853  blpnf  17786  dscopn  17928  itgcn  19029  limcnlp  19060  rngosn3  20923  vtarsuelt  25061  isidlc  25806  lzunuz  26013  dih1  30165
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