Theorem pm5.32i 647

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm5.32ri  648  biadan2  652  anbi2i  705  abai  809  anabs5  823  pm5.33  894  cases  988  equsexvw  1859  equsexv  2077  equsexALT  2142  2sb5rf  2291  2eu8  2400  eq2tri  2523  rexbiia  2900  reubiia  2988  rmobiia  2993  rabbiia  3045  ceqsrexbv  3185  euxfr  3236  2reu5  3260  dfpss3  3531  eldifpr  4002  eldiftp  4027  eldifsn  4110  elrint  4290  elriin  4365  reuxfrd  4642  opeqsn  4714  rabxp  4893  copsex2gb  4967  eliunxp  4994  ressn  5395  dflim2  5502  fncnv  5673  dff1o5  5850  respreima  6037  dff4  6064  dffo3  6065  f1ompt  6072  fsn  6090  fconst3  6158  fconst4  6159  eufnfv  6169  dff13  6189  f1mpt  6192  isocnv3  6253  isores2  6254  isoini  6259  eloprabga  6415  mpt2mptx  6419  resoprab  6424  elrnmpt2res  6442  ov6g  6466  dfwe2  6640  dflim3  6706  dflim4  6707  dfopab2  6879  dfoprab3s  6880  dfoprab3  6881  fparlem1  6928  fparlem2  6929  brtpos2  7010  dftpos3  7022  tpostpos  7024  dfsmo2  7097  dfrecs3  7122  tz7.48-1  7191  ondif1  7234  ondif2  7235  elixp2  7557  mapsnen  7678  xpcomco  7693  eqinf  8031  infempty  8053  r0weon  8474  isinfcard  8554  dfac5lem1  8585  fpwwe  9102  axgroth6  9284  axgroth3  9287  elni2  9333  indpi  9363  recmulnq  9420  genpass  9465  lemul1a  10492  sup3  10599  elnn0z  10984  elznn0  10986  elznn  10987  eluz2b1  11264  eluz2b3  11266  elfz2nn0  11920  elfzo3  11973  shftidt2  13199  clim0  13625  fprod2dlem  14089  divalglem4  14430  ndvdsadd  14444  gcdaddmlem  14547  algfx  14594  isprm3  14688  isprm5  14706  xpsfrnel  15524  isacs2  15614  isfull2  15871  isfth2  15875  tosso  16337  odudlatb  16497  nsgacs  16908  isgim2  16984  isabl2  17493  iscyg3  17576  iscrng2  17851  isdrng2  18040  drngprop  18041  islmim2  18344  islpir2  18530  isnzr2  18542  iunocv  19299  ishil2  19337  islinds2  19426  ssntr  20128  isclo2  20159  isperf2  20223  isperf3  20224  nrmsep3  20426  iscon2  20484  iskgen3  20619  ptpjpre1  20641  tx1cn  20679  tx2cn  20680  hausdiag  20715  qustgplem  21190  istdrg2  21247  isngp2  21666  isngp3  21667  isnvc2  21756  ovoliunlem1  22510  ismbl2  22536  i1f1lem  22703  i1fres  22719  itg1climres  22728  pilem1  23462  ellogrn  23565  ellogdm  23640  1cubr  23824  atandm  23858  atandm2  23859  atandm3  23860  atandm4  23861  atans2  23913  eldmgm  24003  isgrpo2  25981  issubgo  26087  isph  26519  h2hcau  26688  h2hlm  26689  issh2  26918  isch2  26932  h1dei  27259  elbdop2  27580  dfadj2  27594  cnvadj  27601  hhcno  27613  hhcnf  27614  eleigvec2  27667  riesz2  27775  rnbra  27816  elat2  28049  ofpreima  28320  mpt2mptxf  28332  f1od2  28361  maprnin  28368  xrofsup  28405  xrdifh  28414  cmpcref  28728  ofcfval  28970  ispisys2  29026  1stmbfm  29132  2ndmbfm  29133  eulerpartlems  29243  eulerpartlemgc  29245  eulerpartlemv  29247  eulerpartlemd  29249  eulerpartlemr  29257  eulerpartlemn  29264  ballotlemodife  29380  sgn3da  29462  bnj945  29635  bnj1172  29860  bnj1296  29880  snmlval  30104  dfres3  30449  eldm3  30452  nofulllem5  30645  brtxp2  30698  brpprod3a  30703  dffun10  30731  elfuns  30732  brimg  30754  dfrdg4  30768  ellines  30969  opnrebl  31026  bj-ax12ig  31272  bj-equsexval  31297  bj-csbsnlem  31551  bj-mpt2mptALT  31677  bj-elid3  31688  bj-eldiag  31692  taupilem3  31766  topdifinffinlem  31796  relowlssretop  31812  dvtanlemOLD  32037  istotbnd3  32149  isbnd2  32161  isbnd3b  32163  exidcl  32220  isdrngo2  32243  isdrngo3  32244  iscrngo2  32277  isdmn2  32334  isfldidl2  32348  isdmn3  32353  islshpat  32629  iscvlat2N  32936  ishlat3N  32966  snatpsubN  33361  diclspsn  34808  isnacs2  35594  islnm2  35982  islnr2  36019  islnr3  36020  issdrg2  36110  isdomn3  36127  elinintab  36227  elmapintab  36248  elinlem  36250  cnvcnvintabd  36252  isprm7  36705  dffo3f  37504  2reu8  38748  dfdfat2  38768  isodd2  38900  iseven5  38929  isodd7  38930  iscusgrvtx  39635  iscusgredg  39637  ismhm0  40174  sgrp2sgrp  40233  0ringdif  40239  isrnghmmul  40262  eliunxp2  40484  mpt2mptx2  40485  elbigo  40731