Theorem pm5.32i 669

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pm5.32ri  670  biadan2  674  anbi2i  730  abai  836  anabs5  851  pm5.33  922  cases  992  equsexvw  1932  equsexv  2109  equsexALT  2293  2sb5rf  2451  2eu8  2560  eq2tri  2683  rexbiia  3040  reubiia  3127  rmobiia  3132  rabbiia  3185  ceqsrexbv  3337  euxfr  3392  2reu5  3416  dfpss3  3693  eldifpr  4204  eldiftp  4228  eldifsn  4317  elrint  4518  elriin  4593  reuxfrd  4893  opeqsn  4967  rabxp  5154  copsex2gb  5230  eliunxp  5259  dfres3  5403  restidsing  5458  ressn  5671  dflim2  5781  fncnv  5962  dff1o5  6146  respreima  6344  dff4  6373  dffo3  6374  f1ompt  6382  fsn  6402  fconst3  6477  fconst4  6478  eufnfv  6491  dff13  6512  f1mpt  6518  isocnv3  6582  isores2  6583  isoini  6588  eloprabga  6747  mpt2mptx  6751  resoprab  6756  elrnmpt2res  6774  ov6g  6798  dfwe2  6981  dflim3  7047  dflim4  7048  dfopab2  7222  dfoprab3s  7223  dfoprab3  7224  fparlem1  7277  fparlem2  7278  brtpos2  7358  dftpos3  7370  tpostpos  7372  dfsmo2  7444  dfrecs3  7469  tz7.48-1  7538  ondif1  7581  ondif2  7582  elixp2  7912  mapsnen  8035  xpcomco  8050  eqinf  8390  infempty  8412  r0weon  8835  isinfcard  8915  dfac5lem1  8946  fpwwe  9468  axgroth6  9650  axgroth3  9653  elni2  9699  indpi  9729  recmulnq  9786  genpass  9831  lemul1a  10877  sup3  10980  elnn0z  11390  elznn0  11392  elznn  11393  eluz2b1  11759  eluz2b3  11762  elfz2nn0  12431  elfzo3  12486  shftidt2  13821  clim0  14237  fprod2dlem  14710  divalglem4  15119  ndvdsadd  15134  gcdaddmlem  15245  algfx  15293  isprm3  15396  isprm5  15419  isprm7  15420  xpsfrnel  16223  isacs2  16314  isfull2  16571  isfth2  16575  tosso  17036  odudlatb  17196  nsgacs  17630  isgim2  17707  isabl2  18201  iscyg3  18288  iscrng2  18563  isdrng2  18757  drngprop  18758  islmim2  19066  islpir2  19251  isnzr2  19263  iunocv  20025  ishil2  20063  islinds2  20152  ssntr  20862  isclo2  20892  isperf2  20956  isperf3  20957  nrmsep3  21159  isconn2  21217  iskgen3  21352  ptpjpre1  21374  tx1cn  21412  tx2cn  21413  hausdiag  21448  qustgplem  21924  istdrg2  21981  isngp2  22401  isngp3  22402  isnvc2  22503  isclmp  22897  iscvs  22927  isncvsngp  22949  ovoliunlem1  23270  ismbl2  23295  i1f1lem  23456  i1fres  23472  itg1climres  23481  pilem1  24205  ellogrn  24306  ellogdm  24385  1cubr  24569  atandm  24603  atandm2  24604  atandm3  24605  atandm4  24606  atans2  24658  eldmgm  24748  isfusgrcl  26213  iscusgrvtx  26317  iscusgredg  26319  isph  27677  h2hcau  27836  h2hlm  27837  issh2  28066  isch2  28080  h1dei  28409  elbdop2  28730  dfadj2  28744  cnvadj  28751  hhcno  28763  hhcnf  28764  eleigvec2  28817  riesz2  28925  rnbra  28966  elat2  29199  ofpreima  29465  mpt2mptxf  29477  f1od2  29499  maprnin  29506  xrofsup  29533  xrdifh  29542  cmpcref  29917  ofcfval  30160  ispisys2  30216  1stmbfm  30322  2ndmbfm  30323  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemv  30426  eulerpartlemd  30428  eulerpartlemr  30436  eulerpartlemn  30443  ballotlemodife  30559  sgn3da  30603  oddprm2  30733  bnj945  30844  bnj1172  31069  bnj1296  31089  snmlval  31313  eldm3  31651  madeval2  31936  brtxp2  31988  brpprod3a  31993  dffun10  32021  elfuns  32022  brimg  32044  dfrdg4  32058  ellines  32259  opnrebl  32315  bj-ax12ig  32615  bj-equsexval  32638  bj-cleljustab  32847  bj-csbsnlem  32898  bj-mpt2mptALT  33072  bj-elid3  33087  bj-eldiag  33091  taupilem3  33165  topdifinffinlem  33195  relowlssretop  33211  istotbnd3  33570  isbnd2  33582  isbnd3b  33584  exidcl  33675  isdrngo2  33757  isdrngo3  33758  iscrngo2  33796  isdmn2  33854  isfldidl2  33868  isdmn3  33873  brres2  34035  eldmqsres  34051  islshpat  34304  iscvlat2N  34611  ishlat3N  34641  snatpsubN  35036  diclspsn  36483  isnacs2  37269  islnm2  37648  islnr2  37684  islnr3  37685  issdrg2  37768  isdomn3  37782  elinintab  37881  elmapintab  37902  elinlem  37904  cnvcnvintabd  37906  k0004lem1  38445  dffo3f  39364  2reu8  41192  dfdfat2  41211  isodd2  41548  iseven5  41576  isodd7  41577  oddprmne2  41624  ismhm0  41805  sgrp2sgrp  41864  0ringdif  41870  isrnghmmul  41893  eliunxp2  42112  mpt2mptx2  42113  elbigo  42345