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

Theorem pm4.71d 615
 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 611 . 2
31, 2sylib 188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358 This theorem is referenced by:  ax12bOLD  1656  difin2  3430  resopab2  4999  fcnvres  5418  resoprab2  5941  efgcpbllemb  15064  cndis  17019  cnindis  17020  cnpdis  17021  blpnf  17954  dscopn  18096  itgcn  19197  limcnlp  19228  rngosn3  21093  mbfmcnt  23573  vtarsuelt  25895  isidlc  26640  lzunuz  26847  dih1  31476 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360
 Copyright terms: Public domain W3C validator