Theorem pm5.32ri 459

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 458	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi1i  462  pm5.36  618  pm5.61  806  oranabs  827  ceqsralt  2849  ceqsrexbv  2957  reuind  3031  rabsn  3776  dfoprab2  6138  xpsnen  7123  elfpw  7266  sspw1or2  7550  nn1suc  9332  isprm2  12920  ismnd  13791  dfgrp2e  13892  isxms2  15678  clwwlkn1  16864  clwwlkn2  16867  2alsraln0m  17365