MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32i 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  2326  eq2tri  2447  rexbiia  2683  reubiia  2837  rmobiia  2842  rabbiia  2890  ceqsrexbv  3014  euxfr  3064  2reu5  3086  dfpss3  3377  elimif  3712  eldifsn  3871  elrint  4034  elriin  4105  opeqsn  4394  dflim2  4579  reuxfrd  4689  dfwe2  4703  dflim3  4768  dflim4  4769  rabxp  4855  eliunxp  4953  ressn  5349  fncnv  5456  dff1o5  5624  respreima  5799  dff4  5823  dffo3  5824  f1ompt  5831  fsn  5846  fconst3  5895  fconst4  5896  eufnfv  5912  dff13  5944  f1mpt  5947  isocnv3  5992  isores2  5993  isoini  5998  eloprabga  6100  mpt2mptx  6104  resoprab  6106  ov6g  6151  dfopab2  6341  dfoprab3s  6342  dfoprab3  6343  copsex2gb  6347  fparlem1  6386  fparlem2  6387  brtpos2  6422  dftpos3  6434  tpostpos  6436  dfsmo2  6546  tz7.48-1  6637  ondif1  6682  ondif2  6683  elixp2  7003  mapsnen  7121  xpcomco  7135  r0weon  7828  isinfcard  7907  dfac5lem1  7938  fpwwe  8455  axgroth6  8637  axgroth3  8640  elni2  8688  indpi  8718  recmulnq  8775  genpass  8820  lemul1a  9797  sup3  9898  elnn0z  10227  elznn0  10229  elznn  10230  eluz2b1  10480  eluz2b3  10482  elfz2nn0  11015  elfzo3  11086  shftidt2  11824  clim0  12228  divalglem4  12844  ndvdsadd  12856  gcdaddmlem  12956  algfx  12999  isprm3  13016  isprm5  13040  xpsfrnel  13716  isacs2  13806  isfull2  14036  isfth2  14040  tosso  14393  odudlatb  14550  nsgacs  14904  isgim2  14980  isabl2  15348  iscyg3  15424  iscrng2  15607  isdrng2  15773  drngprop  15774  islmim2  16066  islpir2  16250  isnzr2  16262  iunocv  16832  ishil2  16870  istps2OLD  16910  istps3OLD  16911  ssntr  17046  isclo2  17076  isperf2  17139  isperf3  17140  nrmsep3  17342  iscon2  17399  iskgen3  17503  ptpjpre1  17525  tx1cn  17563  tx2cn  17564  hausdiag  17599  divstgplem  18072  istdrg2  18129  isngp2  18516  isngp3  18517  isnvc2  18606  ovoliunlem1  19266  ismbl2  19291  i1f1lem  19449  i1fres  19465  itg1climres  19474  pilem1  20235  ellogrn  20325  ellogdm  20398  1cubr  20550  atandm  20584  atandm2  20585  atandm3  20586  atandm4  20587  atans2  20639  isgrpo2  21634  issubgo  21740  isph  22172  h2hcau  22331  h2hlm  22332  issh2  22560  isch2  22575  h1dei  22901  elbdop2  23223  dfadj2  23237  cnvadj  23244  hhcno  23256  hhcnf  23257  eleigvec2  23310  riesz2  23418  rnbra  23459  elat2  23692  elim2if  23850  xrofsup  23963  xrdifh  23980  eldifpr  24189  eldiftp  24190  ofcfval  24278  1stmbfm  24405  2ndmbfm  24406  ballotlemodife  24535  eldmgm  24586  snmlval  24798  dfres3  25141  eldm3  25144  tfrALTlem  25301  nofulllem5  25385  brtxp2  25446  brpprod3a  25451  elfuns  25479  dfrdg4  25514  ellines  25801  opnrebl  26015  istotbnd3  26172  isbnd2  26184  isbnd3b  26186  exidcl  26243  isdrngo2  26266  isdrngo3  26267  iscrngo2  26300  isdmn2  26357  isfldidl2  26371  isdmn3  26376  isnacs2  26452  islnm2  26846  islinds2  26953  islnr2  26988  islnr3  26989  issdrg2  27176  isdomn3  27193  2reu8  27639  dfdfat2  27665  bnj945  28483  bnj1172  28709  bnj1296  28729  islshpat  29133  iscvlat2N  29440  ishlat3N  29470  snatpsubN  29865  diclspsn  31310
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