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  873  cases  962  2sb5rf  2159  2eu8  2374  eq2tri  2502  rexbiia  2751  reubiia  2909  rmobiia  2914  rabbiia  2964  ceqsrexbv  3097  euxfr  3148  2reu5  3170  dfpss3  3445  eldifpr  3897  eldiftp  3922  eldifsn  4003  elrint  4172  elriin  4246  reuxfrd  4520  opeqsn  4590  dflim2  4778  rabxp  4878  copsex2gb  4953  eliunxp  4980  ressn  5376  fncnv  5485  dff1o5  5653  respreima  5835  dff4  5860  dffo3  5861  f1ompt  5868  fsn  5884  fconst3  5944  fconst4  5945  eufnfv  5954  dff13  5974  f1mpt  5977  isocnv3  6026  isores2  6027  isoini  6032  eloprabga  6180  mpt2mptx  6184  resoprab  6189  elrnmpt2res  6207  ov6g  6231  dfwe2  6396  dflim3  6461  dflim4  6462  dfopab2  6631  dfoprab3s  6632  dfoprab3  6633  fparlem1  6675  fparlem2  6676  brtpos2  6754  dftpos3  6766  tpostpos  6768  dfsmo2  6811  tz7.48-1  6901  ondif1  6944  ondif2  6945  elixp2  7270  mapsnen  7390  xpcomco  7404  r0weon  8182  isinfcard  8265  dfac5lem1  8296  fpwwe  8816  axgroth6  8998  axgroth3  9001  elni2  9049  indpi  9079  recmulnq  9136  genpass  9181  lemul1a  10186  sup3  10290  elnn0z  10662  elznn0  10664  elznn  10665  eluz2b1  10929  eluz2b3  10931  elfz2nn0  11483  elfzo3  11571  shftidt2  12573  clim0  12987  divalglem4  13603  ndvdsadd  13615  gcdaddmlem  13715  algfx  13758  isprm3  13775  isprm5  13801  xpsfrnel  14504  isacs2  14594  isfull2  14824  isfth2  14828  tosso  15209  odudlatb  15369  nsgacs  15720  isgim2  15796  isabl2  16288  iscyg3  16366  iscrng2  16663  isdrng2  16845  drngprop  16846  islmim2  17150  islpir2  17336  isnzr2  17348  iunocv  18109  ishil2  18147  islinds2  18245  istps2OLD  18529  istps3OLD  18530  ssntr  18665  isclo2  18695  isperf2  18759  isperf3  18760  nrmsep3  18962  iscon2  19021  iskgen3  19125  ptpjpre1  19147  tx1cn  19185  tx2cn  19186  hausdiag  19221  divstgplem  19694  istdrg2  19755  isngp2  20192  isngp3  20193  isnvc2  20282  ovoliunlem1  20988  ismbl2  21013  i1f1lem  21170  i1fres  21186  itg1climres  21195  pilem1  21919  ellogrn  22014  ellogdm  22087  1cubr  22240  atandm  22274  atandm2  22275  atandm3  22276  atandm4  22277  atans2  22329  isgrpo2  23687  issubgo  23793  isph  24225  h2hcau  24384  h2hlm  24385  issh2  24614  isch2  24629  h1dei  24956  elbdop2  25278  dfadj2  25292  cnvadj  25299  hhcno  25311  hhcnf  25312  eleigvec2  25365  riesz2  25473  rnbra  25514  elat2  25747  elim2if  25909  ofpreima  25987  mpt2mptxf  25998  f1od2  26027  maprnin  26034  xrofsup  26058  xrdifh  26073  ofcfval  26543  1stmbfm  26678  2ndmbfm  26679  eulerpartlems  26746  eulerpartlemgc  26748  eulerpartlemv  26750  eulerpartlemd  26752  eulerpartlemr  26760  eulerpartlemn  26767  ballotlemodife  26883  sgn3da  26927  eldmgm  27011  snmlval  27223  fprod2dlem  27494  dfres3  27572  eldm3  27575  nofulllem5  27850  brtxp2  27915  brpprod3a  27920  dffun10  27948  elfuns  27949  brimg  27971  dfrdg4  27984  ellines  28186  dvtanlem  28444  opnrebl  28518  istotbnd3  28673  isbnd2  28685  isbnd3b  28687  exidcl  28744  isdrngo2  28767  isdrngo3  28768  iscrngo2  28801  isdmn2  28858  isfldidl2  28872  isdmn3  28877  isnacs2  29045  islnm2  29434  islnr2  29473  islnr3  29474  issdrg2  29558  isdomn3  29575  2reu8  30019  dfdfat2  30040  eliunxp2  30724  mpt2mptx2  30727  bnj945  31770  bnj1172  31995  bnj1296  32015  bj-csbsnlem  32408  bj-eldiag  32529  islshpat  32665  iscvlat2N  32972  ishlat3N  33002  snatpsubN  33397  diclspsn  34842  taupilem3  35615