Theorem pm5.32i 637

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 636	. 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  638  biadan2  642  anbi2i  694  abai  793  anabs5  807  pm5.33  874  cases  964  2sb5rf  2174  2eu8  2389  eq2tri  2528  rexbiia  2957  reubiia  3040  rmobiia  3045  rabbiia  3095  ceqsrexbv  3231  euxfr  3282  2reu5  3305  dfpss3  3583  eldifpr  4037  eldiftp  4063  eldifsn  4145  elrint  4316  elriin  4391  reuxfrd  4665  opeqsn  4736  dflim2  4927  rabxp  5028  copsex2gb  5104  eliunxp  5131  ressn  5534  fncnv  5643  dff1o5  5816  respreima  6001  dff4  6026  dffo3  6027  f1ompt  6034  fsn  6050  fconst3  6115  fconst4  6116  eufnfv  6125  dff13  6145  f1mpt  6148  isocnv3  6207  isores2  6208  isoini  6213  eloprabga  6364  mpt2mptx  6368  resoprab  6373  elrnmpt2res  6391  ov6g  6415  dfwe2  6588  dflim3  6653  dflim4  6654  dfopab2  6828  dfoprab3s  6829  dfoprab3  6830  fparlem1  6873  fparlem2  6874  brtpos2  6951  dftpos3  6963  tpostpos  6965  dfsmo2  7008  tz7.48-1  7098  ondif1  7141  ondif2  7142  elixp2  7463  mapsnen  7583  xpcomco  7597  r0weon  8379  isinfcard  8462  dfac5lem1  8493  fpwwe  9013  axgroth6  9195  axgroth3  9198  elni2  9244  indpi  9274  recmulnq  9331  genpass  9376  lemul1a  10385  sup3  10489  elnn0z  10866  elznn0  10868  elznn  10869  eluz2b1  11142  eluz2b3  11144  elfz2nn0  11757  elfzo3  11801  shftidt2  12864  clim0  13278  divalglem4  13902  ndvdsadd  13914  gcdaddmlem  14014  algfx  14057  isprm3  14074  isprm5  14101  xpsfrnel  14807  isacs2  14897  isfull2  15127  isfth2  15131  tosso  15512  odudlatb  15672  nsgacs  16025  isgim2  16101  isabl2  16595  iscyg3  16673  iscrng2  16994  isdrng2  17182  drngprop  17183  islmim2  17488  islpir2  17674  isnzr2  17686  iunocv  18472  ishil2  18510  islinds2  18608  istps2OLD  19182  istps3OLD  19183  ssntr  19318  isclo2  19348  isperf2  19412  isperf3  19413  nrmsep3  19615  iscon2  19674  iskgen3  19778  ptpjpre1  19800  tx1cn  19838  tx2cn  19839  hausdiag  19874  divstgplem  20347  istdrg2  20408  isngp2  20845  isngp3  20846  isnvc2  20935  ovoliunlem1  21641  ismbl2  21666  i1f1lem  21824  i1fres  21840  itg1climres  21849  pilem1  22573  ellogrn  22668  ellogdm  22741  1cubr  22894  atandm  22928  atandm2  22929  atandm3  22930  atandm4  22931  atans2  22983  isgrpo2  24861  issubgo  24967  isph  25399  h2hcau  25558  h2hlm  25559  issh2  25788  isch2  25803  h1dei  26130  elbdop2  26452  dfadj2  26466  cnvadj  26473  hhcno  26485  hhcnf  26486  eleigvec2  26539  riesz2  26647  rnbra  26688  elat2  26921  elim2if  27082  ofpreima  27165  mpt2mptxf  27176  f1od2  27205  maprnin  27212  xrofsup  27236  xrdifh  27245  ofcfval  27723  1stmbfm  27857  2ndmbfm  27858  eulerpartlems  27925  eulerpartlemgc  27927  eulerpartlemv  27929  eulerpartlemd  27931  eulerpartlemr  27939  eulerpartlemn  27946  ballotlemodife  28062  sgn3da  28106  eldmgm  28190  snmlval  28402  fprod2dlem  28673  dfres3  28751  eldm3  28754  nofulllem5  29029  brtxp2  29094  brpprod3a  29099  dffun10  29127  elfuns  29128  brimg  29150  dfrdg4  29163  ellines  29365  dvtanlem  29628  opnrebl  29702  istotbnd3  29857  isbnd2  29869  isbnd3b  29871  exidcl  29928  isdrngo2  29951  isdrngo3  29952  iscrngo2  29985  isdmn2  30042  isfldidl2  30056  isdmn3  30061  isnacs2  30229  islnm2  30617  islnr2  30656  islnr3  30657  issdrg2  30741  isdomn3  30758  2reu8  31619  dfdfat2  31638  eliunxp2  31862  mpt2mptx2  31863  bnj945  32786  bnj1172  33011  bnj1296  33031  bj-csbsnlem  33426  bj-eldiag  33553  islshpat  33689  iscvlat2N  33996  ishlat3N  34026  snatpsubN  34421  diclspsn  35866  taupilem3  36639