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  7125  elfpw  7268  sspw1or2  7550  nn1suc  9332  isprm2  12919  ismnd  13790  dfgrp2e  13891  isxms2  15695  clwwlkn1  16881  clwwlkn2  16884  2alsraln0m  17382