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

Step	Hyp	Ref	Expression
1		pm5.32i.1	. . 3
2	1	pm5.32i 637	. 2
3		ancom 450	. 2
4		ancom 450	. 2
5	2, 3, 4	3bitr4i 277	1

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