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
Assertion
Ref Expression
pm4.71d

Proof of Theorem pm4.71d
StepHypRef Expression
1 pm4.71rd.1 . 2
2 pm4.71 614 . 2
31, 2sylib 190 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360 This theorem is referenced by:  difin2  3337  resopab2  4906  fcnvres  5275  resoprab2  5793  efgcpbllemb  14899  cndis  16851  cnindis  16852  cnpdis  16853  blpnf  17786  dscopn  17928  itgcn  19029  limcnlp  19060  rngosn3  20923  vtarsuelt  25061  isidlc  25806  lzunuz  26013  dih1  30165 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