Theorem pm5.32i 645

Description: Distribution of implication over biconditional (inference rule).

Hypothesis

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

Assertion

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

Proof of Theorem pm5.32i

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 |- (ph -> (ps <-> ch))
2		pm5.32 644	. 2 |- ((ph -> (ps <-> ch)) <-> ((ph /\ ps) <-> (ph /\ ch)))
3	1, 2	mpbi 189	1 |- ((ph /\ ps) <-> (ph /\ ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm5.32ri 646  pm5.33 650  2eu8 1456  eq2tr 1533  rexbiia 1674  reubiia 1781  rabbii 1805  gencbvex 1838  euxfr 1927  elrabsf 1963  elimif 2374  eldifsn 2462  opeqsn 2802  reuxfr 2904  dflim2 3025  onzsl 3117  dflim4 3119  dfom2 3133  ssrel 3247  iss 3397  fncnv 3561  dff3 3818  dffo3 3819  fsn 3834  fopabap 3841  fconst3 3850  fconst4 3851  f1fv 3874  isoini 3900  tz7.48-1 3956  eloprabg 4007  resoprab 4009  fnoprval 4017  oprabval6g 4032  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  elixp2 4349  mapsnen 4429  abfii2OLD 4562  aceq5lem1 4735  iscard 4853  iscard2 4854  cardval2 4855  isinfcard 4887  elni2 5005  indpi 5034  genpass 5112  reclem1pr 5156  elreal 5250  sup3 6052  elnn0z 6147  elznn0 6149  elznn 6150  elnn0nn 6171  elnnnn0 6172  seq1lem2 6310  dfioo2 6403  serzfsum 7004  serzclim0 7109  infcvglem1 7221  acdcALT 7496  istps2 7607  istps3 7608  lmclim 7963  xplm 7975  opr1scn 7980  bopcnlem1 7981  nvvcop 8213  cnnvm 8313  ip1cnilem4 8376  ip1cnilem6 8378  isph 8481  ipasslem6 8495  pilem1 8671  efifolem5 8726  axgroth3 8779  h2hcau 8849  h2hlm 8850  hilnorm 9030  hcau2 9055  dfchsup2 9298  dfchj2 9324  dfchj3 9325  h1det 9473  elbdop2t 9798  dfadj2 9812  cnvadj 9816  hhlno 9826  bra0 9874  eleigvec2t 9882  riesz2t 9999  rnbra 10040  dfpjopt 10111  elat2 10267  elo 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain