Theorem pm5.32i 641

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm5.32ri  642  biadan2  646  anbi2i  698  abai  802  anabs5  816  pm5.33  886  cases  979  equsexALT  2094  2sb5rf  2247  2eu8  2364  eq2tri  2497  rexbiia  2933  reubiia  3021  rmobiia  3026  rabbiia  3076  ceqsrexbv  3212  euxfr  3263  2reu5  3286  dfpss3  3557  eldifpr  4019  eldiftp  4046  eldifsn  4128  elrint  4300  elriin  4375  reuxfrd  4647  opeqsn  4717  rabxp  4891  copsex2gb  4965  eliunxp  4992  ressn  5392  dflim2  5498  fncnv  5665  dff1o5  5840  respreima  6024  dff4  6051  dffo3  6052  f1ompt  6059  fsn  6076  fconst3  6143  fconst4  6144  eufnfv  6154  dff13  6174  f1mpt  6177  isocnv3  6238  isores2  6239  isoini  6244  eloprabga  6397  mpt2mptx  6401  resoprab  6406  elrnmpt2res  6424  ov6g  6448  dfwe2  6622  dflim3  6688  dflim4  6689  dfopab2  6861  dfoprab3s  6862  dfoprab3  6863  fparlem1  6907  fparlem2  6908  brtpos2  6987  dftpos3  6999  tpostpos  7001  dfsmo2  7074  dfrecs3  7099  tz7.48-1  7168  ondif1  7211  ondif2  7212  elixp2  7534  mapsnen  7654  xpcomco  7668  eqinf  8006  infempty  8022  r0weon  8442  isinfcard  8521  dfac5lem1  8552  fpwwe  9070  axgroth6  9252  axgroth3  9255  elni2  9301  indpi  9331  recmulnq  9388  genpass  9433  lemul1a  10458  sup3  10566  elnn0z  10950  elznn0  10952  elznn  10953  eluz2b1  11230  eluz2b3  11232  elfz2nn0  11883  elfzo3  11934  shftidt2  13123  clim0  13548  fprod2dlem  14012  divalglem4  14352  ndvdsadd  14364  gcdaddmlem  14466  algfx  14510  isprm3  14604  isprm5  14622  xpsfrnel  15420  isacs2  15510  isfull2  15767  isfth2  15771  tosso  16233  odudlatb  16393  nsgacs  16804  isgim2  16880  isabl2  17373  iscyg3  17456  iscrng2  17731  isdrng2  17920  drngprop  17921  islmim2  18224  islpir2  18410  isnzr2  18422  iunocv  19175  ishil2  19213  islinds2  19302  ssntr  20004  isclo2  20035  isperf2  20099  isperf3  20100  nrmsep3  20302  iscon2  20360  iskgen3  20495  ptpjpre1  20517  tx1cn  20555  tx2cn  20556  hausdiag  20591  qustgplem  21066  istdrg2  21123  isngp2  21542  isngp3  21543  isnvc2  21632  ovoliunlem1  22333  ismbl2  22358  i1f1lem  22524  i1fres  22540  itg1climres  22549  pilem1  23271  ellogrn  23374  ellogdm  23449  1cubr  23633  atandm  23667  atandm2  23668  atandm3  23669  atandm4  23670  atans2  23722  eldmgm  23812  isgrpo2  25770  issubgo  25876  isph  26308  h2hcau  26467  h2hlm  26468  issh2  26697  isch2  26711  h1dei  27038  elbdop2  27359  dfadj2  27373  cnvadj  27380  hhcno  27392  hhcnf  27393  eleigvec2  27446  riesz2  27554  rnbra  27595  elat2  27828  ofpreima  28108  mpt2mptxf  28120  f1od2  28152  maprnin  28159  xrofsup  28189  xrdifh  28198  cmpcref  28516  ofcfval  28758  ispisys2  28814  1stmbfm  28921  2ndmbfm  28922  eulerpartlems  29019  eulerpartlemgc  29021  eulerpartlemv  29023  eulerpartlemd  29025  eulerpartlemr  29033  eulerpartlemn  29040  ballotlemodife  29156  sgn3da  29200  bnj945  29373  bnj1172  29598  bnj1296  29618  snmlval  29842  dfres3  30186  eldm3  30189  nofulllem5  30380  brtxp2  30433  brpprod3a  30438  dffun10  30466  elfuns  30467  brimg  30489  dfrdg4  30503  ellines  30704  opnrebl  30761  bj-equsexv  31092  bj-equsexvv  31093  bj-csbsnlem  31255  bj-elid3  31386  bj-eldiag  31391  taupilem3  31465  topdifinffinlem  31484  relowlssretop  31500  dvtanlemOLD  31694  istotbnd3  31806  isbnd2  31818  isbnd3b  31820  exidcl  31877  isdrngo2  31900  isdrngo3  31901  iscrngo2  31934  isdmn2  31991  isfldidl2  32005  isdmn3  32010  islshpat  32291  iscvlat2N  32598  ishlat3N  32628  snatpsubN  33023  diclspsn  34470  isnacs2  35256  islnm2  35641  islnr2  35678  islnr3  35679  issdrg2  35762  isdomn3  35779  isprm7  36296  dffo3f  37072  2reu8  38003  dfdfat2  38022  isodd2  38154  iseven5  38183  isodd7  38184  ismhm0  38562  sgrp2sgrp  38621  0ringdif  38627  isrnghmmul  38650  eliunxp2  38874  mpt2mptx2  38875  elbigo  39122