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  3405  resopab2  4987  fcnvres  5356  resoprab2  5875  efgcpbllemb  15026  cndis  16981  cnindis  16982  cnpdis  16983  blpnf  17916  dscopn  18058  itgcn  19159  limcnlp  19190  rngosn3  21053  vtarsuelt  25262  isidlc  26007  lzunuz  26214  dih1  30643
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