Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32ri Unicode version

Theorem pm5.32ri 638
 Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)
Hypothesis
Ref Expression
pm5.32i.1
Assertion
Ref Expression
pm5.32ri

Proof of Theorem pm5.32ri
StepHypRef Expression
1 pm5.32i.1 . . 3
21pm5.32i 637 . 2
3 ancom 450 . 2
4 ancom 450 . 2
52, 3, 43bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369 This theorem is referenced by:  anbi1i  695  pm5.61  712  oranabs  856  pm5.36  879  2eu5  2382  ceqsralt  3133  ceqsrexbv  3234  reuind  3303  rabsn  4097  reusv2lem4  4656  reusv2lem5  4657  reusv7OLD  4664  dfoprab2  6343  fsplit  6905  xpsnen  7621  elfpw  7842  rankuni  8302  isprm2  14225  ismnd  15923  pjfval2  18740  neipeltop  19630  cmpfi  19908  isxms2  20951  ishl2  21810  usgraop  24350  pjimai  27095  isbndx  30278  pm13.193  31318  bj-snglc  34527  cdlemefrs29pre00  36121  cdlemefrs29cpre1  36124  dihglb2  37069 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