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

Theorem pm5.32ri 619
 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 618 . 2
3 ancom 437 . 2
4 ancom 437 . 2
52, 3, 43bitr4i 268 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358 This theorem is referenced by:  anbi1i  676  pm5.61  693  oranabs  829  pm5.36  849  2eu5  2227  ceqsralt  2811  ceqsrexbv  2902  reuind  2968  rabsn  3697  reusv2lem4  4538  reusv2lem5  4539  reusv7OLD  4546  dfoprab2  5895  fsplit  6223  xpsnen  6946  elfpw  7157  rankuni  7535  isprm2  12766  pjfval2  16609  cmpfi  17135  isxms2  17994  ishl2  18787  pjimai  22756  isbndx  25918  pm13.193  27023  cdlemefrs29pre00  29957  cdlemefrs29cpre1  29960  dihglb2  30905 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