Theorem pm5.32ri 455

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)

Hypothesis

Ref	Expression
pm5.32i.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
pm5.32ri	|- ( ( ps /\ ph ) <-> ( ch /\ ph ) )

Proof of Theorem pm5.32ri

Step	Hyp	Ref	Expression
1		pm5.32i.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	pm5.32i 454	. 2 |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )
3		ancom 266	. 2 |- ( ( ps /\ ph ) <-> ( ph /\ ps ) )
4		ancom 266	. 2 |- ( ( ch /\ ph ) <-> ( ph /\ ch ) )
5	2, 3, 4	3bitr4i 212	1 |- ( ( ps /\ ph ) <-> ( ch /\ ph ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi1i  458  pm5.36  614  pm5.61  801  oranabs  822  ceqsralt  2830  ceqsrexbv  2937  reuind  3011  rabsn  3736  dfoprab2  6067  xpsnen  7004  sspw1or2  7402  nn1suc  9161  isprm2  12688  ismnd  13501  dfgrp2e  13610  isxms2  15175  clwwlkn1  16268  clwwlkn2  16271