Theorem pm5.32i 648

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 647	. 2 |- ((ph -> (ps <-> ch)) <-> ((ph /\ ps) <-> (ph /\ ch)))
3	1, 2	mpbi 187	1 |- ((ph /\ ps) <-> (ph /\ ch))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  pm5.32ri 649  pm5.33 653  2eu8 1496  eq2tri 1576  rexbiia 1720  reubiia 1827  rabbii 1851  gencbvex 1884  euxfr 1973  elrabsf 2011  elimif 2428  eldifsn 2526  opeqsn 2879  dflim2 3029  reuxfr 3127  onzsl 3200  dflim4 3202  dfom2 3220  ssrel 3334  ssrelrel 3340  iss 3487  fncnv 3666  dff4 3932  dffo3 3933  fsn 3948  fopabap 3955  fconst3 3964  fconst4 3965  dff13 3988  isoini 4014  eloprabg 4067  resoprab 4069  fnoprv 4077  oprabval6g 4093  dfopab2 4173  dfoprab3 4174  dfoprab3s 4175  fparlem1 4199  fparlem2 4200  tz7.48-1 4257  elixp2 4490  mapsnen 4570  abfii2 4705  aceq5lem1 4881  iscard 5003  iscard2 5004  cardval2 5005  isinfcard 5037  elni2 5159  indpi 5188  genpass 5266  reclem1pr 5310  elreal 5404  sup3 6220  elnn0z 6315  elznn0 6317  elznn 6318  elnn0nn 6339  elnnnn0 6340  dfioo2 6530  seq1lem2 6675  serzfsum 7207  serzclim0 7312  infcvglem1 7425  acdcALT 7708  istps2 7819  istps3 7820  lmclim 8174  xplm 8186  opr1scn 8191  bopcnlem1 8192  nvvcop 8460  cnnvm 8560  ip1cnilem4 8630  ip1cnilem6 8632  isph 8737  ipasslem6 8751  pilem1 8938  efifolem5 8998  axgroth3 9051  h2hcau 9124  h2hlm 9125  hilnormi 9306  hcau2 9331  dfchsup2 9574  dfchj2 9600  dfchj3 9601  h1dei 9749  elbdop2 10078  dfadj2 10092  cnvadj 10096  hhlnoi 10106  bra0 10154  eleigvec2 10162  riesz2 10278  rnbra 10320  dfpjop 10391  elat2 10548  elo 10733  isufil2 11650  respreima 11795  piececn 11955  isbnd3 11997  heiborlem24 12034  heiborlem29 12039  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096

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 145  df-an 223

Copyright terms: Public domain