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

Theorem pm5.32da 622
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
pm5.32da  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21ex 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 620 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  rexbida  2558  reubida  2722  rmobida  2727  mpteq12f  4096  reuhypd  4561  funbrfv2b  5567  dffn5  5568  eqfnfv2  5623  fmptco  5691  dff13  5783  mpt2eq123dva  5909  mpt2eq3dva  5912  fnwelem  6230  opiota  6290  riotabidva  6321  oeeui  6600  omabs  6645  qliftfun  6743  erovlem  6754  xpcomco  6952  pw2f1olem  6966  elfi2  7168  cardval2  7624  dfac2  7757  cflim3  7888  iundom2g  8162  fpwwe2lem8  8259  fpwwe2lem12  8263  ltexpi  8526  ordpipq  8566  axrrecex  8785  nnunb  9961  zrevaddcl  10063  qrevaddcl  10338  icoshft  10758  fznn  10852  fznnfl  10966  fz1isolem  11399  2shfti  11575  limsupgle  11951  ello12  11990  elo12  12001  isercoll  12141  sumeq2ii  12166  fsum2dlem  12233  bitsmod  12627  bitscmp  12629  pwsle  13391  imasleval  13443  acsfiel  13556  ismon2  13637  isepi2  13644  oppcsect  13676  subsubc  13727  funcpropd  13774  fullpropd  13794  fucsect  13846  setcsect  13921  pltval3  14101  ismgmid  14387  grpidpropd  14399  mhmpropd  14421  issubm2  14426  subgacs  14652  eqgid  14669  pgpfi2  14917  eqgabl  15131  iscyggen2  15168  cyggenod  15171  eldprd  15239  subgdmdprd  15269  dprd2d2  15279  rngpropd  15372  crngunit  15444  dvdsrpropd  15478  drngpropd  15539  issubrg3  15573  lsslss  15718  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  aspval2  16086  znleval  16508  znunithash  16518  pjdm2  16611  bastop2  16732  elcls2  16811  maxlp  16878  restopn2  16908  iscnp3  16974  subbascn  16984  lmbr2  16989  kgencn  17251  kgencn2  17252  hauseqlcld  17340  txlm  17342  txkgen  17346  xkoptsub  17348  idqtop  17397  tgqtop  17403  qtopcld  17404  elmptrab  17522  flimopn  17670  fbflim  17671  fbflim2  17672  flimrest  17678  flffbas  17690  flftg  17691  cnflf  17697  cnflf2  17698  txflf  17701  isfcls  17704  fclsopn  17709  fclsbas  17716  fclsrest  17719  fcfnei  17730  cnfcf  17737  ptcmplem2  17747  tgphaus  17799  tsmssubm  17825  ismet2  17898  xblpnf  17953  blin  17970  blres  17977  elmopn2  17991  imasf1obl  18034  imasf1oxms  18035  prdsbl  18037  neibl  18047  metrest  18070  metcnp3  18086  metcnp  18087  metcnp2  18088  metcn  18089  txmetcnp  18093  txmetcn  18094  ngppropd  18153  cnbl0  18283  cnblcld  18284  bl2ioo  18298  xrtgioo  18312  elcncf2  18394  cncfmet  18412  nmhmcn  18601  lmmbr  18684  lmmbr2  18685  iscfil2  18692  iscau2  18703  iscau3  18704  lmclim  18728  shft2rab  18867  sca2rab  18871  mbfeqalem  18997  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  i1fmullem  19049  i1fmulclem  19057  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  ibllem  19119  ellimc2  19227  ellimc3  19229  limcflf  19231  cnplimc  19237  cnlimc  19238  dvreslem  19259  ply1remlem  19548  fta1glem2  19552  ofmulrt  19662  plyremlem  19684  ulm2  19764  mcubic  20143  cubic2  20144  dvdsflsumcom  20428  fsumvma  20452  fsumvma2  20453  vmasum  20455  logfaclbnd  20461  dchrelbas2  20476  dchrelbas3  20477  dchrelbas4  20482  lgsquadlem1  20593  lgsquadlem2  20594  isblo2  21361  ubthlem1  21449  h2hlm  21560  pjpreeq  21977  elnlfn  22508  reuxfr4d  23139  itgeq12dv  23196  feqmptdf  23228  fmptcof2  23229  gsumpropd2lem  23379  orvcgteel  23668  eupath2  23904  dfrdg2  24152  preduz  24200  predfz  24203  broutsideof3  24749  areacirclem6  24930  surjsec2  25120  prodeq3ii  25308  svs2  25487  svs3  25488  isfne4b  26270  filnetlem4  26330  isdrngo3  26590  isidlc  26640  prter3  26750  ellz1  26846  rmydioph  27107  rmxdioph  27109  expdiophlem1  27114  expdioph  27116  pw2f1ocnv  27130  dnwech  27145  islinds2  27283  sdrgacs  27509  pm14.123b  27626  rfcnpre1  27690  rfcnpre2  27702  rfcnpre3  27704  rfcnpre4  27705  climreeq  27739  funbrafv2b  28021  dfafn5a  28022  mpt2xopovel  28086  nbgrael  28141  nbcusgra  28159  islshpsm  29170  islshpat  29207  lkrsc  29287  lfl1dim  29311  ldual1dim  29356  isat3  29497  glbconxN  29567  islln2  29700  islpln2  29725  islvol2  29769  cdlemg2cex  30780  diaglbN  31245  diblsmopel  31361  dihopelvalcpre  31438  xihopellsmN  31444  dihopellsm  31445  dihglbcpreN  31490  mapdval4N  31822  hdmapoc  32124
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