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  2096  2sb5rf  2250  2eu8  2359  eq2tri  2490  rexbiia  2923  reubiia  3011  rmobiia  3016  rabbiia  3068  ceqsrexbv  3205  euxfr  3256  2reu5  3280  dfpss3  3551  eldifpr  4020  eldiftp  4043  eldifsn  4125  elrint  4297  elriin  4372  reuxfrd  4646  opeqsn  4716  rabxp  4890  copsex2gb  4964  eliunxp  4991  ressn  5391  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  6990  dftpos3  7002  tpostpos  7004  dfsmo2  7077  dfrecs3  7102  tz7.48-1  7171  ondif1  7214  ondif2  7215  elixp2  7537  mapsnen  7657  xpcomco  7671  eqinf  8009  infempty  8031  r0weon  8451  isinfcard  8530  dfac5lem1  8561  fpwwe  9078  axgroth6  9260  axgroth3  9263  elni2  9309  indpi  9339  recmulnq  9396  genpass  9441  lemul1a  10466  sup3  10573  elnn0z  10957  elznn0  10959  elznn  10960  eluz2b1  11237  eluz2b3  11239  elfz2nn0  11892  elfzo3  11943  shftidt2  13144  clim0  13569  fprod2dlem  14033  divalglem4  14374  ndvdsadd  14388  gcdaddmlem  14491  algfx  14538  isprm3  14632  isprm5  14650  xpsfrnel  15468  isacs2  15558  isfull2  15815  isfth2  15819  tosso  16281  odudlatb  16441  nsgacs  16852  isgim2  16928  isabl2  17437  iscyg3  17520  iscrng2  17795  isdrng2  17984  drngprop  17985  islmim2  18288  islpir2  18474  isnzr2  18486  iunocv  19242  ishil2  19280  islinds2  19369  ssntr  20071  isclo2  20102  isperf2  20166  isperf3  20167  nrmsep3  20369  iscon2  20427  iskgen3  20562  ptpjpre1  20584  tx1cn  20622  tx2cn  20623  hausdiag  20658  qustgplem  21133  istdrg2  21190  isngp2  21609  isngp3  21610  isnvc2  21699  ovoliunlem1  22453  ismbl2  22479  i1f1lem  22645  i1fres  22661  itg1climres  22670  pilem1  23404  ellogrn  23507  ellogdm  23582  1cubr  23766  atandm  23800  atandm2  23801  atandm3  23802  atandm4  23803  atans2  23855  eldmgm  23945  isgrpo2  25923  issubgo  26029  isph  26461  h2hcau  26630  h2hlm  26631  issh2  26860  isch2  26874  h1dei  27201  elbdop2  27522  dfadj2  27536  cnvadj  27543  hhcno  27555  hhcnf  27556  eleigvec2  27609  riesz2  27717  rnbra  27758  elat2  27991  ofpreima  28270  mpt2mptxf  28282  f1od2  28315  maprnin  28322  xrofsup  28359  xrdifh  28368  cmpcref  28685  ofcfval  28927  ispisys2  28983  1stmbfm  29090  2ndmbfm  29091  eulerpartlems  29201  eulerpartlemgc  29203  eulerpartlemv  29205  eulerpartlemd  29207  eulerpartlemr  29215  eulerpartlemn  29222  ballotlemodife  29338  sgn3da  29420  bnj945  29593  bnj1172  29818  bnj1296  29838  snmlval  30062  dfres3  30406  eldm3  30409  nofulllem5  30600  brtxp2  30653  brpprod3a  30658  dffun10  30686  elfuns  30687  brimg  30709  dfrdg4  30723  ellines  30924  opnrebl  30981  bj-equsexv  31311  bj-equsexvv  31312  bj-csbsnlem  31474  bj-elid3  31605  bj-eldiag  31610  taupilem3  31684  topdifinffinlem  31714  relowlssretop  31730  dvtanlemOLD  31955  istotbnd3  32067  isbnd2  32079  isbnd3b  32081  exidcl  32138  isdrngo2  32161  isdrngo3  32162  iscrngo2  32195  isdmn2  32252  isfldidl2  32266  isdmn3  32271  islshpat  32552  iscvlat2N  32859  ishlat3N  32889  snatpsubN  33284  diclspsn  34731  isnacs2  35517  islnm2  35906  islnr2  35943  islnr3  35944  issdrg2  36034  isdomn3  36051  elinintab  36151  elmapintab  36172  elinlem  36174  cnvcnvintabd  36176  isprm7  36630  dffo3f  37411  2reu8  38484  dfdfat2  38503  isodd2  38635  iseven5  38664  isodd7  38665  iscusgrvtx  39246  iscusgredg  39248  ismhm0  39425  sgrp2sgrp  39484  0ringdif  39490  isrnghmmul  39513  eliunxp2  39737  mpt2mptx2  39738  elbigo  39984