Theorem pm5.32i 632

Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  pm5.32ri  633  biadan2  637  anbi2i  689  abai  788  anabs5  802  pm5.33  868  cases  957  2sb5rf  2164  2eu8  2373  eq2tri  2500  rexbiia  2746  reubiia  2904  rmobiia  2909  rabbiia  2959  ceqsrexbv  3091  euxfr  3142  2reu5  3164  dfpss3  3439  eldifpr  3891  eldiftp  3916  eldifsn  3997  elrint  4166  elriin  4240  reuxfrd  4514  opeqsn  4584  dflim2  4771  rabxp  4871  copsex2gb  4946  eliunxp  4973  ressn  5370  fncnv  5479  dff1o5  5647  respreima  5829  dff4  5854  dffo3  5855  f1ompt  5862  fsn  5878  fconst3  5938  fconst4  5939  eufnfv  5948  dff13  5968  f1mpt  5971  isocnv3  6020  isores2  6021  isoini  6026  eloprabga  6176  mpt2mptx  6180  resoprab  6185  elrnmpt2res  6203  ov6g  6227  dfwe2  6392  dflim3  6457  dflim4  6458  dfopab2  6627  dfoprab3s  6628  dfoprab3  6629  fparlem1  6671  fparlem2  6672  brtpos2  6750  dftpos3  6762  tpostpos  6764  dfsmo2  6804  tz7.48-1  6894  ondif1  6937  ondif2  6938  elixp2  7263  mapsnen  7383  xpcomco  7397  r0weon  8175  isinfcard  8258  dfac5lem1  8289  fpwwe  8809  axgroth6  8991  axgroth3  8994  elni2  9042  indpi  9072  recmulnq  9129  genpass  9174  lemul1a  10179  sup3  10283  elnn0z  10655  elznn0  10657  elznn  10658  eluz2b1  10922  eluz2b3  10924  elfz2nn0  11476  elfzo3  11564  shftidt2  12566  clim0  12980  divalglem4  13596  ndvdsadd  13608  gcdaddmlem  13708  algfx  13751  isprm3  13768  isprm5  13794  xpsfrnel  14497  isacs2  14587  isfull2  14817  isfth2  14821  tosso  15202  odudlatb  15362  nsgacs  15710  isgim2  15786  isabl2  16278  iscyg3  16356  iscrng2  16650  isdrng2  16822  drngprop  16823  islmim2  17125  islpir2  17311  isnzr2  17323  iunocv  18065  ishil2  18103  islinds2  18201  istps2OLD  18485  istps3OLD  18486  ssntr  18621  isclo2  18651  isperf2  18715  isperf3  18716  nrmsep3  18918  iscon2  18977  iskgen3  19081  ptpjpre1  19103  tx1cn  19141  tx2cn  19142  hausdiag  19177  divstgplem  19650  istdrg2  19711  isngp2  20148  isngp3  20149  isnvc2  20238  ovoliunlem1  20944  ismbl2  20969  i1f1lem  21126  i1fres  21142  itg1climres  21151  pilem1  21875  ellogrn  21970  ellogdm  22043  1cubr  22196  atandm  22230  atandm2  22231  atandm3  22232  atandm4  22233  atans2  22285  isgrpo2  23619  issubgo  23725  isph  24157  h2hcau  24316  h2hlm  24317  issh2  24546  isch2  24561  h1dei  24888  elbdop2  25210  dfadj2  25224  cnvadj  25231  hhcno  25243  hhcnf  25244  eleigvec2  25297  riesz2  25405  rnbra  25446  elat2  25679  elim2if  25841  ofpreima  25919  mpt2mptxf  25930  f1od2  25959  maprnin  25966  xrofsup  25988  xrdifh  26003  ofcfval  26476  1stmbfm  26611  2ndmbfm  26612  eulerpartlems  26673  eulerpartlemgc  26675  eulerpartlemv  26677  eulerpartlemd  26679  eulerpartlemr  26687  eulerpartlemn  26694  ballotlemodife  26810  sgn3da  26854  eldmgm  26938  snmlval  27150  fprod2dlem  27420  dfres3  27498  eldm3  27501  nofulllem5  27776  brtxp2  27841  brpprod3a  27846  dffun10  27874  elfuns  27875  brimg  27897  dfrdg4  27910  ellines  28112  dvtanlem  28366  opnrebl  28440  istotbnd3  28595  isbnd2  28607  isbnd3b  28609  exidcl  28666  isdrngo2  28689  isdrngo3  28690  iscrngo2  28723  isdmn2  28780  isfldidl2  28794  isdmn3  28799  isnacs2  28967  islnm2  29356  islnr2  29395  islnr3  29396  issdrg2  29480  isdomn3  29497  2reu8  29941  dfdfat2  29962  eliunxp2  30645  mpt2mptx2  30648  bnj945  31601  bnj1172  31826  bnj1296  31846  bj-csbsnlem  32143  bj-eldiag  32255  islshpat  32384  iscvlat2N  32691  ishlat3N  32721  snatpsubN  33116  diclspsn  34561  taupilem3  35334