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

Theorem pm5.32da 651
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 440 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 649 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  rexbida  2868  rexbidva  2870  reubida  2941  rmobida  2946  mpteq12f  4451  reuhypd  4600  xpdifid  5243  funbrfv2b  5892  dffn5  5893  feqmptdf  5903  eqfnfv2  5961  fmptco  6041  dff13  6145  riotabidva  6254  mpt2eq123dva  6340  mpt2eq3dva  6343  opiota  6840  fnwelem  6899  suppssr  6934  mpt2xopovel  6954  mpt2curryd  7003  oeeui  7290  omabs  7335  qliftfun  7435  erovlem  7446  xpcomco  7649  pw2f1olem  7663  elfi2  7915  cardval2  8412  dfac2  8548  cflim3  8679  iundom2g  8952  fpwwe2lem8  9049  fpwwe2lem12  9053  ltexpi  9314  ordpipq  9354  axrrecex  9574  nnunb  10855  zrevaddcl  10972  qrevaddcl  11276  icoshft  11745  fznn  11854  preduz  11904  predfz  11907  fznnfl  12083  fz1isolem  12619  swrdeq  12799  2swrdeqwrdeq  12808  2swrd1eqwrdeq  12809  2swrd2eqwrdeq  13039  2shfti  13154  limsupgle  13546  ello12  13591  elo12  13602  isercoll  13742  sumeq2ii  13770  fsum2dlem  13842  prodeq2ii  13978  bitsmod  14421  bitscmp  14423  pwsle  15401  imasleval  15458  acsfiel  15571  ismon2  15650  isepi2  15657  oppcsect  15694  subsubc  15769  funcpropd  15816  fullpropd  15836  fucsect  15888  setcsect  15995  pltval3  16224  grpidpropd  16515  ismgmid  16518  gsumpropd2lem  16527  mhmpropd  16599  issubm2  16606  subgacs  16863  eqgid  16880  pgpfi2  17269  eqgabl  17486  iscyggen2  17527  cyggenod  17530  eldprd  17647  subgdmdprd  17678  dprd2d2  17688  ringpropd  17823  crngunit  17901  dvdsrpropd  17935  drngpropd  18013  issubrg3  18047  lsslss  18195  lsspropd  18251  lmhmpropd  18307  lbspropd  18333  aspval2  18582  znleval  19136  znunithash  19146  pjdm2  19285  islinds2  19382  bastop2  20021  elcls2  20101  neiptopreu  20160  maxlp  20174  restopn2  20204  iscnp3  20271  subbascn  20281  lmbr2  20286  kgencn  20582  kgencn2  20583  hauseqlcld  20672  txlm  20674  txkgen  20678  xkoptsub  20680  idqtop  20732  tgqtop  20738  qtopcld  20739  elmptrab  20853  flimopn  21001  fbflim  21002  fbflim2  21003  flimrest  21009  flffbas  21021  flftg  21022  cnflf  21028  cnflf2  21029  txflf  21032  isfcls  21035  fclsopn  21040  fclsbas  21047  fclsrest  21050  fcfnei  21061  cnfcf  21068  ptcmplem2  21079  tgphaus  21142  tsmssubm  21168  isucn2  21305  ismet2  21359  xblpnfps  21421  xblpnf  21422  blin  21447  blres  21457  elmopn2  21471  imasf1obl  21514  imasf1oxms  21515  prdsbl  21517  neibl  21527  metrest  21550  metcnp3  21566  metcnp  21567  metcnp2  21568  metcn  21569  txmetcnp  21573  txmetcn  21574  metuel2  21591  metucn  21597  ngppropd  21656  cnbl0  21805  cnblcld  21806  bl2ioo  21821  xrtgioo  21835  elcncf2  21933  cncfmet  21951  nmhmcn  22145  lmmbr  22239  lmmbr2  22240  iscfil2  22247  iscau2  22258  iscau3  22259  lmclim  22283  shft2rab  22472  sca2rab  22476  mbfeqalem  22610  mbfmulc2lem  22615  mbfmax  22617  mbfposr  22620  mbfimaopnlem  22623  mbfaddlem  22628  mbfsup  22632  mbfinf  22633  mbfinfOLD  22634  i1fmullem  22664  i1fmulclem  22672  i1fres  22675  itg1climres  22684  mbfi1fseqlem4  22688  ibllem  22734  ellimc2  22844  ellimc3  22846  limcflf  22848  cnplimc  22854  cnlimc  22855  dvreslem  22876  ply1remlem  23125  fta1glem2  23129  ofmulrt  23247  plyremlem  23269  ulm2  23352  mcubic  23785  cubic2  23786  dvdsflsumcom  24129  fsumvma  24153  fsumvma2  24154  vmasum  24156  logfaclbnd  24162  dchrelbas2  24177  dchrelbas3  24178  dchrelbas4  24183  lgsquadlem1  24294  lgsquadlem2  24295  colopp  24823  colhp  24824  nbgrael  25166  nbcusgra  25203  clwwlkn2  25515  el2wlkonotot1  25614  usg2spthonot0  25629  eupath2  25720  isblo2  26436  ubthlem1  26524  h2hlm  26645  pjpreeq  27063  elnlfn  27593  reuxfr4d  28138  fmptcof2  28267  funcnvmpt  28279  fpwrelmapffslem  28325  nndiffz1  28374  smatrcl  28629  ismntop  28837  itgeq12dv  29165  eulerpartlemgvv  29215  orvcgteel  29306  dfrdg2  30448  broutsideof3  30899  isfne4b  31003  filnetlem4  31043  poimirlem23  31965  poimirlem26  31968  poimirlem27  31969  heicant  31977  cnambfre  31991  itg2gt0cn  31999  ftc1anclem5  32023  areacirclem5  32038  isdrngo3  32200  isidlc  32250  prter3  32456  islshpsm  32548  islshpat  32585  lkrsc  32665  lfl1dim  32689  ldual1dim  32734  isat3  32875  glbconxN  32945  islln2  33078  islpln2  33103  islvol2  33147  cdlemg2cex  34160  diaglbN  34625  diblsmopel  34741  dihopelvalcpre  34818  xihopellsmN  34824  dihopellsm  34825  dihglbcpreN  34870  mapdval4N  35202  hdmapoc  35504  ellz1  35611  rmydioph  35871  rmxdioph  35873  expdiophlem1  35878  expdioph  35880  pw2f1ocnv  35894  dnwech  35908  sdrgacs  36069  pm14.123b  36778  rfcnpre1  37337  rfcnpre2  37349  rfcnpre3  37351  rfcnpre4  37352  climreeq  37735  funbrafv2b  38752  dfafn5a  38753  pfxeq  39038  pfxsuffeqwrdeq  39040  pfxsuff1eqwrdeq  39041  nbgrel  39512  umgr2v2enb1  39665  mgmhmpropd  40110  issubmgm2  40115  isrnghmmul  40218  rngcsect  40307  rngcsectALTV  40319  ringcsect  40358  ringcsectALTV  40382  elbigo2  40688
  Copyright terms: Public domain W3C validator