Theorem pm5.32i 635

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 634	. 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 367

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 369

This theorem is referenced by:  pm5.32ri  636  biadan2  640  anbi2i  692  abai  793  anabs5  807  pm5.33  876  cases  968  2sb5rf  2199  2eu8  2317  eq2tri  2450  rexbiia  2883  reubiia  2968  rmobiia  2973  rabbiia  3023  ceqsrexbv  3159  euxfr  3210  2reu5  3233  dfpss3  3504  eldifpr  3961  eldiftp  3987  eldifsn  4069  elrint  4241  elriin  4316  reuxfrd  4587  opeqsn  4657  dflim2  4848  rabxp  4950  copsex2gb  5026  eliunxp  5053  ressn  5452  fncnv  5560  dff1o5  5733  respreima  5918  dff4  5947  dffo3  5948  f1ompt  5955  fsn  5971  fconst3  6036  fconst4  6037  eufnfv  6047  dff13  6067  f1mpt  6070  isocnv3  6129  isores2  6130  isoini  6135  eloprabga  6288  mpt2mptx  6292  resoprab  6297  elrnmpt2res  6315  ov6g  6339  dfwe2  6516  dflim3  6581  dflim4  6582  dfopab2  6753  dfoprab3s  6754  dfoprab3  6755  fparlem1  6799  fparlem2  6800  brtpos2  6879  dftpos3  6891  tpostpos  6893  dfsmo2  6936  tz7.48-1  7026  ondif1  7069  ondif2  7070  elixp2  7392  mapsnen  7512  xpcomco  7526  r0weon  8303  isinfcard  8386  dfac5lem1  8417  fpwwe  8935  axgroth6  9117  axgroth3  9120  elni2  9166  indpi  9196  recmulnq  9253  genpass  9298  lemul1a  10313  sup3  10416  elnn0z  10794  elznn0  10796  elznn  10797  eluz2b1  11072  eluz2b3  11074  elfz2nn0  11691  elfzo3  11738  shftidt2  12916  clim0  13331  fprod2dlem  13786  divalglem4  14056  ndvdsadd  14068  gcdaddmlem  14168  algfx  14211  isprm3  14228  isprm5  14255  xpsfrnel  14970  isacs2  15060  isfull2  15317  isfth2  15321  tosso  15783  odudlatb  15943  nsgacs  16354  isgim2  16430  isabl2  16923  iscyg3  17006  iscrng2  17327  isdrng2  17519  drngprop  17520  islmim2  17825  islpir2  18012  isnzr2  18024  iunocv  18803  ishil2  18841  islinds2  18933  istps2OLD  19507  istps3OLD  19508  ssntr  19644  isclo2  19675  isperf2  19739  isperf3  19740  nrmsep3  19942  iscon2  20000  iskgen3  20135  ptpjpre1  20157  tx1cn  20195  tx2cn  20196  hausdiag  20231  qustgplem  20704  istdrg2  20765  isngp2  21202  isngp3  21203  isnvc2  21292  ovoliunlem1  21998  ismbl2  22023  i1f1lem  22181  i1fres  22197  itg1climres  22206  pilem1  22931  ellogrn  23032  ellogdm  23107  1cubr  23289  atandm  23323  atandm2  23324  atandm3  23325  atandm4  23326  atans2  23378  isgrpo2  25316  issubgo  25422  isph  25854  h2hcau  26013  h2hlm  26014  issh2  26243  isch2  26258  h1dei  26585  elbdop2  26906  dfadj2  26920  cnvadj  26927  hhcno  26939  hhcnf  26940  eleigvec2  26993  riesz2  27101  rnbra  27142  elat2  27375  ofpreima  27653  mpt2mptxf  27665  f1od2  27697  maprnin  27704  xrofsup  27735  xrdifh  27744  cmpcref  28007  ofcfval  28246  ispisys2  28302  1stmbfm  28387  2ndmbfm  28388  eulerpartlems  28482  eulerpartlemgc  28484  eulerpartlemv  28486  eulerpartlemd  28488  eulerpartlemr  28496  eulerpartlemn  28503  ballotlemodife  28619  sgn3da  28663  eldmgm  28753  snmlval  28965  dfres3  29354  eldm3  29357  nofulllem5  29631  brtxp2  29684  brpprod3a  29689  dffun10  29717  elfuns  29718  brimg  29740  dfrdg4  29753  ellines  29955  dvtanlemOLD  30230  opnrebl  30304  istotbnd3  30433  isbnd2  30445  isbnd3b  30447  exidcl  30504  isdrngo2  30527  isdrngo3  30528  iscrngo2  30561  isdmn2  30618  isfldidl2  30632  isdmn3  30637  isnacs2  30804  islnm2  31190  islnr2  31231  islnr3  31232  issdrg2  31315  isdomn3  31332  isprm7  31360  2reu8  32363  dfdfat2  32382  isodd2  32478  iseven5  32507  isodd7  32508  ismhm0  32811  sgrp2sgrp  32870  0ringdif  32876  isrnghmmul  32899  eliunxp2  33123  mpt2mptx2  33124  elbigo  33372  bnj945  34179  bnj1172  34404  bnj1296  34424  bj-csbsnlem  34817  bj-elid3  34949  bj-eldiag  34954  islshpat  35155  iscvlat2N  35462  ishlat3N  35492  snatpsubN  35887  diclspsn  37334  taupilem3  38107