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  2243  eq2tri  2355  rexbiia  2589  reubiia  2738  rmobiia  2743  rabbiia  2791  ceqsrexbv  2915  euxfr  2964  2reu5  2986  dfpss3  3275  elimif  3607  eldifsn  3762  elrint  3919  elriin  3990  opeqsn  4278  dflim2  4464  reuxfrd  4575  dfwe2  4589  dflim3  4654  dflim4  4655  rabxp  4741  eliunxp  4839  ressn  5227  fncnv  5330  dff1o5  5497  respreima  5670  dff4  5690  dffo3  5691  f1ompt  5698  fsn  5712  fconst3  5751  fconst4  5752  eufnfv  5768  dff13  5799  f1mpt  5801  isocnv3  5845  isores2  5846  isoini  5851  eloprabga  5950  mpt2mptx  5954  resoprab  5956  ov6g  6001  dfopab2  6190  dfoprab3s  6191  dfoprab3  6192  copsex2gb  6196  fparlem1  6234  fparlem2  6235  brtpos2  6256  dftpos3  6268  tpostpos  6270  dfsmo2  6380  tz7.48-1  6471  ondif1  6516  ondif2  6517  elixp2  6836  mapsnen  6954  xpcomco  6968  r0weon  7656  isinfcard  7735  dfac5lem1  7766  fpwwe  8284  axgroth6  8466  axgroth3  8469  elni2  8517  indpi  8547  recmulnq  8604  genpass  8649  lemul1a  9626  sup3  9727  elnn0z  10052  elznn0  10054  elznn  10055  eluz2b1  10305  eluz2b3  10307  elfz2nn0  10837  elfzo3  10906  shftidt2  11592  clim0  11996  divalglem4  12611  ndvdsadd  12623  gcdaddmlem  12723  algfx  12766  isprm3  12783  isprm5  12807  xpsfrnel  13481  isacs2  13571  isfull2  13801  isfth2  13805  tosso  14158  odudlatb  14315  nsgacs  14669  isgim2  14745  isabl2  15113  iscyg3  15189  iscrng2  15372  isdrng2  15538  drngprop  15539  islmim2  15835  islpir2  16019  isnzr2  16031  iunocv  16597  ishil2  16635  istps2OLD  16675  istps3OLD  16676  ssntr  16811  isclo2  16841  isperf2  16899  isperf3  16900  nrmsep3  17099  iscon2  17156  iskgen3  17260  ptpjpre1  17282  tx1cn  17319  tx2cn  17320  hausdiag  17355  divstgplem  17819  istdrg2  17876  isngp2  18135  isngp3  18136  isnvc2  18225  ovoliunlem1  18877  ismbl2  18902  i1f1lem  19060  i1fres  19076  itg1climres  19085  pilem1  19843  ellogrn  19933  ellogdm  20002  1cubr  20154  atandm  20188  atandm2  20189  atandm3  20190  atandm4  20191  atans2  20243  isgrpo2  20880  issubgo  20986  isph  21416  h2hcau  21575  h2hlm  21576  issh2  21804  isch2  21819  h1dei  22145  elbdop2  22467  dfadj2  22481  cnvadj  22488  hhcno  22500  hhcnf  22501  eleigvec2  22554  riesz2  22662  rnbra  22703  elat2  22936  ballotlemodife  23072  elim2if  23168  xrofsup  23270  xrdifh  23288  eldifpr  23409  eldiftp  23410  ofcfval  23474  1stmbfm  23580  2ndmbfm  23581  eldmgm  23709  snmlval  23929  dfres3  24187  eldm3  24190  tfrALTlem  24347  nofulllem5  24431  brtxp2  24492  brpprod3a  24497  elfuns  24525  dfrdg4  24560  ellines  24847  dfoprab4pop  25140  elo  25144  dff1o6f  25195  isdir2  25395  issubcata  25949  opnrebl  26338  istotbnd3  26598  isbnd2  26610  isbnd3b  26612  exidcl  26669  isdrngo2  26692  isdrngo3  26693  iscrngo2  26726  isdmn2  26783  isfldidl2  26797  isdmn3  26802  isnacs2  26884  islnm2  27279  islinds2  27386  islnr2  27421  islnr3  27422  issdrg2  27609  isdomn3  27626  2reu8  28073  dfdfat2  28099  bnj945  29121  bnj1172  29347  bnj1296  29367  islshpat  29829  iscvlat2N  30136  ishlat3N  30166  snatpsubN  30561  diclspsn  32006
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