MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71d 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
Assertion
Ref Expression
pm4.71d

Proof of Theorem pm4.71d
StepHypRef Expression
1 pm4.71rd.1 . 2
2 pm4.71 630 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  difin2  3759  resopab2  5327  fcnvres  5767  resoprab2  6399  psgnran  16540  efgcpbllemb  16773  cndis  19792  cnindis  19793  cnpdis  19794  blpnf  20900  dscopn  21094  itgcn  22249  limcnlp  22282  nb3gra2nb  24455  usg2wlkeq  24708  clwwlkn2  24775  rngosn3  25428  1stpreima  27524  fsumcvg4  27932  mbfmcnt  28239  ptrest  30048  isidlc  30412  lzunuz  30701  dih1  37013
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
  Copyright terms: Public domain W3C validator