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:  ax12b  1834  difin2  3372  resopab2  4952  fcnvres  5321  resoprab2  5840  efgcpbllemb  14991  cndis  16946  cnindis  16947  cnpdis  16948  blpnf  17881  dscopn  18023  itgcn  19124  limcnlp  19155  rngosn3  21018  vtarsuelt  25227  isidlc  25972  lzunuz  26179  dih1  30606
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