Theorem pm5.32i 707

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm5.32ri 708  pm5.33 712  2eu8 1860  eq2tri 1956  rexbiia 2134  reubiia 2261  rabbiia 2285  gencbvexOLD 2335  euxfr 2438  elrabsf 2486  dfpss3 2695  elimif 3001  eldifsn 3123  opeqsn 3549  dflim2 3719  reuxfrd 3846  dfwe2 3861  onzslOLD 3929  dflim3 3930  dflim4 3932  dfom2 3951  ssrelOLD 4076  ssrelrelOLD 4084  issOLD 4255  fncnv 4479  dff1o5 4646  eufnfv 4771  dff4 4791  dffo3 4792  fsn 4807  fopabap 4817  fconst3 4826  fconst4 4827  dff13 4850  isoini 4877  eloprabg 4936  resoprab 4938  fnoprv 4946  oprabval6g 4962  dfopab2 5053  dfoprab3 5054  dfoprab3s 5055  fparlem1 5081  fparlem2 5082  tz7.48-1 5165  elixp2 5408  mapsnen 5488  abfii2 5652  aceq5lem1 5897  iscard 6005  iscard2 6006  cardval2 6007  isinfcard 6035  elni2 6157  indpi 6186  genpass 6264  reclem1pr 6308  elreal 6402  sup3 7261  elnn0z 7356  elznn0 7358  elznn 7359  elnn0nn 7380  elnnnn0 7381  dfioo2 7572  seq1lem2 7723  serzfsum 8264  serzclim0 8369  infcvglem1 8482  acdcALT 8765  istps2 8876  istps3 8877  lmclim 9241  xplm 9253  opr1scn 9258  bopcnlem1 9259  nvvcop 9545  cnnvm 9645  ip1cnilem4 9715  ip1cnilem6 9717  isph 9822  ipasslem6 9836  pilem1 10020  efifolem5 10080  axgroth6 10137  axgroth3 10138  h2hcau 10481  h2hlm 10482  hilnormi 10663  hcau2 10688  dfchsup2 10931  dfchj2 10957  dfchj3 10958  h1dei 11106  elbdop2 11435  dfadj2 11449  cnvadj 11453  hhlnoi 11463  bra0 11511  eleigvec2 11519  riesz2 11636  rnbra 11678  dfpjop 11755  elat2 11912  bnj141 12473  bnj945 12844  bnj1298 13043  bnj1172 13440  divalglem4 13699  ndvdsadd 13711  gcdaddmlem 13734  algfx 13748  zgt1b1 13771  zgt1b2 13772  isprm3 13776  tfrALTlem 13976  fnoprvpop 14338  elo 14342  isdir2 14640  svs2 14829  svs3 14830  ttcn 14913  invtrgrp 14979  topgrpsubcnlem 14981  cntrsetlem 14999  isufil2 15565  biadan2 15648  respreima 15684  idcncf 15884  piececn 15894  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  isbnd3 15941  heiborlem24 15978  heiborlem29 15983  exidcl 16029  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcohtpylem3 16082  pcopt 16084  isdivrng2 16111  isdivrng3 16112  iscring2 16146  isdmn2 16203  isfldidl2 16217  isdmn3 16222  pointpsub 17231

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 164  df-an 242

Copyright terms: Public domain