MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32i Structured version   Unicode version

Theorem pm5.32i 619
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
StepHypRef Expression
1 pm5.32i.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 pm5.32 618 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
31, 2mpbi 200 1  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm5.32ri  620  biadan2  624  anbi2i  676  abai  771  anabs5  785  pm5.33  849  2eu8  2367  eq2tri  2494  rexbiia  2730  reubiia  2885  rmobiia  2890  rabbiia  2938  ceqsrexbv  3062  euxfr  3112  2reu5  3134  dfpss3  3425  elimif  3760  eldifsn  3919  elrint  4083  elriin  4155  opeqsn  4444  dflim2  4629  reuxfrd  4740  dfwe2  4754  dflim3  4819  dflim4  4820  rabxp  4906  eliunxp  5004  ressn  5400  fncnv  5507  dff1o5  5675  respreima  5851  dff4  5875  dffo3  5876  f1ompt  5883  fsn  5898  fconst3  5947  fconst4  5948  eufnfv  5964  dff13  5996  f1mpt  5999  isocnv3  6044  isores2  6045  isoini  6050  eloprabga  6152  mpt2mptx  6156  resoprab  6158  ov6g  6203  dfopab2  6393  dfoprab3s  6394  dfoprab3  6395  copsex2gb  6399  fparlem1  6438  fparlem2  6439  brtpos2  6477  dftpos3  6489  tpostpos  6491  dfsmo2  6601  tz7.48-1  6692  ondif1  6737  ondif2  6738  elixp2  7058  mapsnen  7176  xpcomco  7190  r0weon  7886  isinfcard  7965  dfac5lem1  7996  fpwwe  8513  axgroth6  8695  axgroth3  8698  elni2  8746  indpi  8776  recmulnq  8833  genpass  8878  lemul1a  9856  sup3  9957  elnn0z  10286  elznn0  10288  elznn  10289  eluz2b1  10539  eluz2b3  10541  elfz2nn0  11074  elfzo3  11147  shftidt2  11888  clim0  12292  divalglem4  12908  ndvdsadd  12920  gcdaddmlem  13020  algfx  13063  isprm3  13080  isprm5  13104  xpsfrnel  13780  isacs2  13870  isfull2  14100  isfth2  14104  tosso  14457  odudlatb  14614  nsgacs  14968  isgim2  15044  isabl2  15412  iscyg3  15488  iscrng2  15671  isdrng2  15837  drngprop  15838  islmim2  16130  islpir2  16314  isnzr2  16326  iunocv  16900  ishil2  16938  istps2OLD  16978  istps3OLD  16979  ssntr  17114  isclo2  17144  isperf2  17208  isperf3  17209  nrmsep3  17411  iscon2  17469  iskgen3  17573  ptpjpre1  17595  tx1cn  17633  tx2cn  17634  hausdiag  17669  divstgplem  18142  istdrg2  18199  isngp2  18636  isngp3  18637  isnvc2  18726  ovoliunlem1  19390  ismbl2  19415  i1f1lem  19573  i1fres  19589  itg1climres  19598  pilem1  20359  ellogrn  20449  ellogdm  20522  1cubr  20674  atandm  20708  atandm2  20709  atandm3  20710  atandm4  20711  atans2  20763  isgrpo2  21777  issubgo  21883  isph  22315  h2hcau  22474  h2hlm  22475  issh2  22703  isch2  22718  h1dei  23044  elbdop2  23366  dfadj2  23380  cnvadj  23387  hhcno  23399  hhcnf  23400  eleigvec2  23453  riesz2  23561  rnbra  23602  elat2  23835  elim2if  23997  ofpreima  24073  xrofsup  24118  xrdifh  24135  eldifpr  24384  eldiftp  24385  ofcfval  24473  1stmbfm  24602  2ndmbfm  24603  ballotlemodife  24747  eldmgm  24798  snmlval  25010  fprod2dlem  25296  dfres3  25374  eldm3  25377  nofulllem5  25653  brtxp2  25718  brpprod3a  25723  dffun10  25751  elfuns  25752  brimg  25774  dfrdg4  25787  ellines  26078  opnrebl  26314  istotbnd3  26471  isbnd2  26483  isbnd3b  26485  exidcl  26542  isdrngo2  26565  isdrngo3  26566  iscrngo2  26599  isdmn2  26656  isfldidl2  26670  isdmn3  26675  isnacs2  26751  islnm2  27144  islinds2  27251  islnr2  27286  islnr3  27287  issdrg2  27474  isdomn3  27491  2reu8  27937  dfdfat2  27962  bnj945  29081  bnj1172  29307  bnj1296  29327  islshpat  29752  iscvlat2N  30059  ishlat3N  30089  snatpsubN  30484  diclspsn  31929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator