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  1681  difin2  3464  resopab2  5036  fcnvres  5456  resoprab2  5983  efgcpbllemb  15113  cndis  17075  cnindis  17076  cnpdis  17077  blpnf  18006  dscopn  18148  itgcn  19250  limcnlp  19281  rngosn3  21146  1stpreima  23245  mbfmcnt  23792  isidlc  25788  lzunuz  25995  nb3gra2nb  27401  dih1  31294 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