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

Theorem pm5.32da 639
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 432 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 637 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  rexbida  2960  rexbidva  2962  reubida  3037  rmobida  3042  mpteq12f  4515  reuhypd  4664  xpdifid  5420  funbrfv2b  5892  dffn5  5893  eqfnfv2  5958  fmptco  6040  dff13  6141  riotabidva  6248  mpt2eq123dva  6331  mpt2eq3dva  6334  opiota  6832  fnwelem  6888  suppssr  6923  mpt2xopovel  6940  mpt2curryd  6990  oeeui  7243  omabs  7288  qliftfun  7388  erovlem  7399  xpcomco  7600  pw2f1olem  7614  elfi2  7866  cardval2  8363  dfac2  8502  cflim3  8633  iundom2g  8906  fpwwe2lem8  9004  fpwwe2lem12  9008  ltexpi  9269  ordpipq  9309  axrrecex  9529  nnunb  10787  zrevaddcl  10905  qrevaddcl  11205  icoshft  11645  fznn  11751  fznnfl  11971  fz1isolem  12494  swrdeq  12660  2swrdeqwrdeq  12669  2swrd1eqwrdeq  12670  2swrd2eqwrdeq  12882  2shfti  12995  limsupgle  13382  ello12  13421  elo12  13432  isercoll  13572  sumeq2ii  13597  fsum2dlem  13667  prodeq2ii  13802  bitsmod  14170  bitscmp  14172  pwsle  14981  imasleval  15030  acsfiel  15143  ismon2  15222  isepi2  15229  oppcsect  15266  subsubc  15341  funcpropd  15388  fullpropd  15408  fucsect  15460  setcsect  15567  pltval3  15796  grpidpropd  16087  ismgmid  16090  gsumpropd2lem  16099  mhmpropd  16171  issubm2  16178  subgacs  16435  eqgid  16452  pgpfi2  16825  eqgabl  17042  iscyggen2  17083  cyggenod  17086  eldprd  17230  eldprdOLD  17232  subgdmdprd  17276  dprd2d2  17288  ringpropd  17425  crngunit  17506  dvdsrpropd  17540  drngpropd  17618  issubrg3  17652  lsslss  17802  lsspropd  17858  lmhmpropd  17914  lbspropd  17940  aspval2  18191  znleval  18766  znunithash  18776  pjdm2  18915  islinds2  19015  bastop2  19663  elcls2  19742  neiptopreu  19801  maxlp  19815  restopn2  19845  iscnp3  19912  subbascn  19922  lmbr2  19927  kgencn  20223  kgencn2  20224  hauseqlcld  20313  txlm  20315  txkgen  20319  xkoptsub  20321  idqtop  20373  tgqtop  20379  qtopcld  20380  elmptrab  20494  flimopn  20642  fbflim  20643  fbflim2  20644  flimrest  20650  flffbas  20662  flftg  20663  cnflf  20669  cnflf2  20670  txflf  20673  isfcls  20676  fclsopn  20681  fclsbas  20688  fclsrest  20691  fcfnei  20702  cnfcf  20709  ptcmplem2  20719  tgphaus  20781  tsmssubm  20810  isucn2  20948  ismet2  21002  xblpnfps  21064  xblpnf  21065  blin  21090  blres  21100  elmopn2  21114  imasf1obl  21157  imasf1oxms  21158  prdsbl  21160  neibl  21170  metrest  21193  metcnp3  21209  metcnp  21210  metcnp2  21211  metcn  21212  txmetcnp  21216  txmetcn  21217  metuel2  21248  metucnOLD  21257  metucn  21258  ngppropd  21317  cnbl0  21447  cnblcld  21448  bl2ioo  21463  xrtgioo  21477  elcncf2  21560  cncfmet  21578  nmhmcn  21769  lmmbr  21863  lmmbr2  21864  iscfil2  21871  iscau2  21882  iscau3  21883  lmclim  21907  shft2rab  22085  sca2rab  22089  mbfeqalem  22215  mbfmulc2lem  22220  mbfmax  22222  mbfposr  22225  mbfimaopnlem  22228  mbfaddlem  22233  mbfsup  22237  mbfinf  22238  i1fmullem  22267  i1fmulclem  22275  i1fres  22278  itg1climres  22287  mbfi1fseqlem4  22291  ibllem  22337  ellimc2  22447  ellimc3  22449  limcflf  22451  cnplimc  22457  cnlimc  22458  dvreslem  22479  ply1remlem  22729  fta1glem2  22733  ofmulrt  22844  plyremlem  22866  ulm2  22946  mcubic  23375  cubic2  23376  dvdsflsumcom  23662  fsumvma  23686  fsumvma2  23687  vmasum  23689  logfaclbnd  23695  dchrelbas2  23710  dchrelbas3  23711  dchrelbas4  23716  lgsquadlem1  23827  lgsquadlem2  23828  nbgrael  24628  nbcusgra  24665  clwwlkn2  24977  el2wlkonotot1  25076  usg2spthonot0  25091  eupath2  25182  isblo2  25896  ubthlem1  25984  h2hlm  26095  pjpreeq  26514  elnlfn  27045  reuxfr4d  27587  feqmptdf  27723  fmptcof2  27724  funcnvmpt  27737  fpwrelmapffslem  27786  nndiffz1  27830  ismntop  28238  itgeq12dv  28532  eulerpartlemgvv  28579  orvcgteel  28670  dfrdg2  29468  preduz  29520  predfz  29523  broutsideof3  30004  heicant  30289  cnambfre  30303  itg2gt0cn  30310  ftc1anclem5  30334  areacirclem5  30351  isfne4b  30399  filnetlem4  30439  isdrngo3  30602  isidlc  30652  prter3  30863  ellz1  30939  rmydioph  31195  rmxdioph  31197  expdiophlem1  31202  expdioph  31204  pw2f1ocnv  31218  dnwech  31233  sdrgacs  31391  pm14.123b  31574  rfcnpre1  31634  rfcnpre2  31646  rfcnpre3  31648  rfcnpre4  31649  climreeq  31858  funbrafv2b  32483  dfafn5a  32484  pfxeq  32632  pfxsuffeqwrdeq  32634  pfxsuff1eqwrdeq  32635  mgmhmpropd  32845  issubmgm2  32850  isrnghmmul  32953  rngcsect  33042  rngcsectALTV  33054  ringcsect  33093  ringcsectALTV  33117  elbigo2  33427  islshpsm  35102  islshpat  35139  lkrsc  35219  lfl1dim  35243  ldual1dim  35288  isat3  35429  glbconxN  35499  islln2  35632  islpln2  35657  islvol2  35701  cdlemg2cex  36714  diaglbN  37179  diblsmopel  37295  dihopelvalcpre  37372  xihopellsmN  37378  dihopellsm  37379  dihglbcpreN  37424  mapdval4N  37756  hdmapoc  38058
  Copyright terms: Public domain W3C validator