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

Theorem pm5.32i 618
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 617 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
31, 2mpbi 199 1  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm5.32ri  619  biadan2  623  anbi2i  675  abai  770  anabs5  784  pm5.33  848  2eu8  2230  eq2tri  2342  rexbiia  2576  reubiia  2725  rmobiia  2730  rabbiia  2778  ceqsrexbv  2902  euxfr  2951  2reu5  2973  dfpss3  3262  elimif  3594  eldifsn  3749  elrint  3903  elriin  3974  opeqsn  4262  dflim2  4448  reuxfrd  4559  dfwe2  4573  dflim3  4638  dflim4  4639  rabxp  4725  eliunxp  4823  ressn  5211  fncnv  5314  dff1o5  5481  respreima  5654  dff4  5674  dffo3  5675  f1ompt  5682  fsn  5696  fconst3  5735  fconst4  5736  eufnfv  5752  dff13  5783  f1mpt  5785  isocnv3  5829  isores2  5830  isoini  5835  eloprabga  5934  mpt2mptx  5938  resoprab  5940  ov6g  5985  dfopab2  6174  dfoprab3s  6175  dfoprab3  6176  copsex2gb  6180  fparlem1  6218  fparlem2  6219  brtpos2  6240  dftpos3  6252  tpostpos  6254  dfsmo2  6364  tz7.48-1  6455  ondif1  6500  ondif2  6501  elixp2  6820  mapsnen  6938  xpcomco  6952  r0weon  7640  isinfcard  7719  dfac5lem1  7750  fpwwe  8268  axgroth6  8450  axgroth3  8453  elni2  8501  indpi  8531  recmulnq  8588  genpass  8633  lemul1a  9610  sup3  9711  elnn0z  10036  elznn0  10038  elznn  10039  eluz2b1  10289  eluz2b3  10291  elfz2nn0  10821  elfzo3  10890  shftidt2  11576  clim0  11980  divalglem4  12595  ndvdsadd  12607  gcdaddmlem  12707  algfx  12750  isprm3  12767  isprm5  12791  xpsfrnel  13465  isacs2  13555  isfull2  13785  isfth2  13789  tosso  14142  odudlatb  14299  nsgacs  14653  isgim2  14729  isabl2  15097  iscyg3  15173  iscrng2  15356  isdrng2  15522  drngprop  15523  islmim2  15819  islpir2  16003  isnzr2  16015  iunocv  16581  ishil2  16619  istps2OLD  16659  istps3OLD  16660  ssntr  16795  isclo2  16825  isperf2  16883  isperf3  16884  nrmsep3  17083  iscon2  17140  iskgen3  17244  ptpjpre1  17266  tx1cn  17303  tx2cn  17304  hausdiag  17339  divstgplem  17803  istdrg2  17860  isngp2  18119  isngp3  18120  isnvc2  18209  ovoliunlem1  18861  ismbl2  18886  i1f1lem  19044  i1fres  19060  itg1climres  19069  pilem1  19827  ellogrn  19917  ellogdm  19986  1cubr  20138  atandm  20172  atandm2  20173  atandm3  20174  atandm4  20175  atans2  20227  isgrpo2  20864  issubgo  20970  isph  21400  h2hcau  21559  h2hlm  21560  issh2  21788  isch2  21803  h1dei  22129  elbdop2  22451  dfadj2  22465  cnvadj  22472  hhcno  22484  hhcnf  22485  eleigvec2  22538  riesz2  22646  rnbra  22687  elat2  22920  ballotlemodife  23056  elim2if  23152  xrofsup  23255  xrdifh  23273  eldifpr  23394  eldiftp  23395  ofcfval  23459  1stmbfm  23565  2ndmbfm  23566  eldmgm  23694  snmlval  23914  dfres3  24116  eldm3  24119  tfrALTlem  24276  nofulllem5  24360  brtxp2  24421  brpprod3a  24426  elfuns  24454  dfrdg4  24488  ellines  24775  dfoprab4pop  25037  elo  25041  dff1o6f  25092  isdir2  25292  issubcata  25846  opnrebl  26235  istotbnd3  26495  isbnd2  26507  isbnd3b  26509  exidcl  26566  isdrngo2  26589  isdrngo3  26590  iscrngo2  26623  isdmn2  26680  isfldidl2  26694  isdmn3  26699  isnacs2  26781  islnm2  27176  islinds2  27283  islnr2  27318  islnr3  27319  issdrg2  27506  isdomn3  27523  2reu8  27970  dfdfat2  27994  bnj945  28805  bnj1172  29031  bnj1296  29051  islshpat  29207  iscvlat2N  29514  ishlat3N  29544  snatpsubN  29939  diclspsn  31384
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 177  df-an 360
  Copyright terms: Public domain W3C validator