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  795  anabs5  809  pm5.33  878  cases  970  2sb5rf  2181  2eu8  2372  eq2tri  2511  rexbiia  2944  reubiia  3029  rmobiia  3034  rabbiia  3084  ceqsrexbv  3220  euxfr  3271  2reu5  3294  dfpss3  3575  eldifpr  4031  eldiftp  4057  eldifsn  4140  elrint  4313  elriin  4388  reuxfrd  4662  opeqsn  4733  dflim2  4924  rabxp  5026  copsex2gb  5103  eliunxp  5130  ressn  5533  fncnv  5642  dff1o5  5815  respreima  6001  dff4  6030  dffo3  6031  f1ompt  6038  fsn  6054  fconst3  6120  fconst4  6121  eufnfv  6131  dff13  6151  f1mpt  6154  isocnv3  6213  isores2  6214  isoini  6219  eloprabga  6374  mpt2mptx  6378  resoprab  6383  elrnmpt2res  6401  ov6g  6425  dfwe2  6602  dflim3  6667  dflim4  6668  dfopab2  6839  dfoprab3s  6840  dfoprab3  6841  fparlem1  6885  fparlem2  6886  brtpos2  6963  dftpos3  6975  tpostpos  6977  dfsmo2  7020  tz7.48-1  7110  ondif1  7153  ondif2  7154  elixp2  7475  mapsnen  7595  xpcomco  7609  r0weon  8393  isinfcard  8476  dfac5lem1  8507  fpwwe  9027  axgroth6  9209  axgroth3  9212  elni2  9258  indpi  9288  recmulnq  9345  genpass  9390  lemul1a  10402  sup3  10506  elnn0z  10883  elznn0  10885  elznn  10886  eluz2b1  11162  eluz2b3  11164  elfz2nn0  11777  elfzo3  11823  shftidt2  12893  clim0  13308  divalglem4  13931  ndvdsadd  13943  gcdaddmlem  14043  algfx  14086  isprm3  14103  isprm5  14130  xpsfrnel  14837  isacs2  14927  isfull2  15154  isfth2  15158  tosso  15540  odudlatb  15700  nsgacs  16111  isgim2  16187  isabl2  16680  iscyg3  16763  iscrng2  17088  isdrng2  17280  drngprop  17281  islmim2  17586  islpir2  17773  isnzr2  17785  iunocv  18585  ishil2  18623  islinds2  18721  istps2OLD  19295  istps3OLD  19296  ssntr  19432  isclo2  19462  isperf2  19526  isperf3  19527  nrmsep3  19729  iscon2  19788  iskgen3  19923  ptpjpre1  19945  tx1cn  19983  tx2cn  19984  hausdiag  20019  qustgplem  20492  istdrg2  20553  isngp2  20990  isngp3  20991  isnvc2  21080  ovoliunlem1  21786  ismbl2  21811  i1f1lem  21969  i1fres  21985  itg1climres  21994  pilem1  22718  ellogrn  22819  ellogdm  22892  1cubr  23045  atandm  23079  atandm2  23080  atandm3  23081  atandm4  23082  atans2  23134  isgrpo2  25071  issubgo  25177  isph  25609  h2hcau  25768  h2hlm  25769  issh2  25998  isch2  26013  h1dei  26340  elbdop2  26662  dfadj2  26676  cnvadj  26683  hhcno  26695  hhcnf  26696  eleigvec2  26749  riesz2  26857  rnbra  26898  elat2  27131  ofpreima  27379  mpt2mptxf  27390  f1od2  27419  maprnin  27426  xrofsup  27454  xrdifh  27463  cmpcref  27726  ofcfval  27970  1stmbfm  28104  2ndmbfm  28105  eulerpartlems  28172  eulerpartlemgc  28174  eulerpartlemv  28176  eulerpartlemd  28178  eulerpartlemr  28186  eulerpartlemn  28193  ballotlemodife  28309  sgn3da  28353  eldmgm  28437  snmlval  28649  fprod2dlem  29085  dfres3  29163  eldm3  29166  nofulllem5  29441  brtxp2  29506  brpprod3a  29511  dffun10  29539  elfuns  29540  brimg  29562  dfrdg4  29575  ellines  29777  dvtanlem  30039  opnrebl  30113  istotbnd3  30242  isbnd2  30254  isbnd3b  30256  exidcl  30313  isdrngo2  30336  isdrngo3  30337  iscrngo2  30370  isdmn2  30427  isfldidl2  30441  isdmn3  30446  isnacs2  30613  islnm2  30999  islnr2  31038  islnr3  31039  issdrg2  31123  isdomn3  31140  isprm7  31168  2reu8  32035  dfdfat2  32054  sgrp2sgrp  32389  isrnghmmul  32417  eliunxp2  32656  mpt2mptx2  32657  bnj945  33565  bnj1172  33790  bnj1296  33810  bj-csbsnlem  34218  bj-elid3  34341  bj-eldiag  34346  islshpat  34482  iscvlat2N  34789  ishlat3N  34819  snatpsubN  35214  diclspsn  36661  taupilem3  37434