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

Theorem pm5.32da 674
 Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
pm5.32da (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 672 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  rexbida  3076  rexbidva  3078  reubida  3154  rmobida  3159  mpteq12f  4764  reuhypd  4925  xpdifid  5597  funbrfv2b  6279  dffn5  6280  feqmptdf  6290  eqfnfv2  6352  fmptco  6436  dff13  6552  riotabidva  6667  mpt2eq123dva  6758  mpt2eq3dva  6761  opiota  7273  fnwelem  7337  suppssr  7371  mpt2xopovel  7391  mpt2curryd  7440  oeeui  7727  omabs  7772  qliftfun  7875  erovlem  7886  xpcomco  8091  pw2f1olem  8105  elfi2  8361  cardval2  8855  dfac2  8991  cflim3  9122  iundom2g  9400  fpwwe2lem8  9497  fpwwe2lem12  9501  ltexpi  9762  ordpipq  9802  axrrecex  10022  nnunb  11326  zrevaddcl  11460  qrevaddcl  11848  icoshft  12332  fznn  12446  preduz  12500  predfz  12503  fznnfl  12701  fz1isolem  13283  swrdeq  13490  2swrdeqwrdeq  13499  2swrd1eqwrdeq  13500  2swrd2eqwrdeq  13742  eqwrds3  13750  2shfti  13864  limsupgle  14252  ello12  14291  elo12  14302  isercoll  14442  sumeq2ii  14467  fsum2dlem  14545  prodeq2ii  14687  bitsmod  15205  bitscmp  15207  pwsle  16199  imasleval  16248  acsfiel  16362  ismon2  16441  isepi2  16448  oppcsect  16485  subsubc  16560  funcpropd  16607  fullpropd  16627  fucsect  16679  setcsect  16786  pltval3  17014  grpidpropd  17308  ismgmid  17311  gsumpropd2lem  17320  mhmpropd  17388  issubm2  17395  subgacs  17676  eqgid  17693  pgpfi2  18067  eqgabl  18286  iscyggen2  18329  cyggenod  18332  eldprd  18449  subgdmdprd  18479  dprd2d2  18489  ringpropd  18628  crngunit  18708  dvdsrpropd  18742  drngpropd  18822  issubrg3  18856  lsslss  19009  lsspropd  19065  lmhmpropd  19121  lbspropd  19147  aspval2  19395  znleval  19951  znunithash  19961  pjdm2  20103  islinds2  20200  bastop2  20846  elcls2  20926  neiptopreu  20985  maxlp  20999  restopn2  21029  iscnp3  21096  subbascn  21106  lmbr2  21111  kgencn  21407  kgencn2  21408  hauseqlcld  21497  txlm  21499  txkgen  21503  xkoptsub  21505  idqtop  21557  tgqtop  21563  qtopcld  21564  elmptrab  21678  flimopn  21826  fbflim  21827  fbflim2  21828  flimrest  21834  flffbas  21846  flftg  21847  cnflf  21853  cnflf2  21854  txflf  21857  isfcls  21860  fclsopn  21865  fclsbas  21872  fclsrest  21875  fcfnei  21886  cnfcf  21893  ptcmplem2  21904  tgphaus  21967  tsmssubm  21993  isucn2  22130  ismet2  22185  xblpnfps  22247  xblpnf  22248  blin  22273  blres  22283  elmopn2  22297  imasf1obl  22340  imasf1oxms  22341  prdsbl  22343  neibl  22353  metrest  22376  metcnp3  22392  metcnp  22393  metcnp2  22394  metcn  22395  txmetcnp  22399  txmetcn  22400  metuel2  22417  metucn  22423  ngppropd  22488  cnbl0  22624  cnblcld  22625  bl2ioo  22642  xrtgioo  22656  elcncf2  22740  cncfmet  22758  nmhmcn  22966  lmmbr  23102  lmmbr2  23103  iscfil2  23110  iscau2  23121  iscau3  23122  lmclim  23147  shft2rab  23322  sca2rab  23326  mbfeqalem  23454  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  mbfimaopnlem  23467  mbfaddlem  23472  mbfsup  23476  mbfinf  23477  i1fmullem  23506  i1fmulclem  23514  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  ibllem  23576  ellimc2  23686  ellimc3  23688  limcflf  23690  cnplimc  23696  cnlimc  23697  dvreslem  23718  ply1remlem  23967  fta1glem2  23971  ofmulrt  24082  plyremlem  24104  ulm2  24184  mcubic  24619  cubic2  24620  dvdsflsumcom  24959  fsumvma  24983  fsumvma2  24984  vmasum  24986  logfaclbnd  24992  dchrelbas2  25007  dchrelbas3  25008  dchrelbas4  25013  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1a  25161  colopp  25706  colhp  25707  nbgrelOLD  26279  umgr2v2enb1  26478  upgriswlk  26593  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  elwwlks2on  26925  elwwlks2  26933  elwspths2spth  26934  isclwwlknx  26998  clwwlkn1  27004  clwwlkn2  27007  eupth2lems  27216  fusgr2wsp2nb  27314  numclwwlkqhash  27355  isblo2  27766  ubthlem1  27854  h2hlm  27965  pjpreeq  28385  elnlfn  28915  reuxfr4d  29457  fmptcof2  29585  funcnvmpt  29596  fpwrelmapffslem  29635  nndiffz1  29676  smatrcl  29990  ismntop  30198  itgeq12dv  30516  eulerpartlemgvv  30566  orvcgteel  30657  reprinrn  30824  reprdifc  30833  dfrdg2  31825  broutsideof3  32358  isfne4b  32461  filnetlem4  32501  uncf  33518  poimirlem23  33562  poimirlem26  33565  poimirlem27  33566  heicant  33574  cnambfre  33588  itg2gt0cn  33595  ftc1anclem5  33619  areacirclem5  33634  isdrngo3  33888  isidlc  33944  prter3  34486  islshpsm  34585  islshpat  34622  lkrsc  34702  lfl1dim  34726  ldual1dim  34771  isat3  34912  glbconxN  34982  islln2  35115  islpln2  35140  islvol2  35184  cdlemg2cex  36196  diaglbN  36661  diblsmopel  36777  dihopelvalcpre  36854  xihopellsmN  36860  dihopellsm  36861  dihglbcpreN  36906  mapdval4N  37238  hdmapoc  37540  ellz1  37647  rmydioph  37898  rmxdioph  37900  expdiophlem1  37905  expdioph  37907  pw2f1ocnv  37921  dnwech  37935  sdrgacs  38088  rfovcnvf1od  38615  k0004lem3  38764  pm14.123b  38944  rfcnpre1  39492  rfcnpre2  39504  rfcnpre3  39506  rfcnpre4  39507  climreeq  40163  funbrafv2b  41560  dfafn5a  41561  pfxeq  41729  pfxsuffeqwrdeq  41731  pfxsuff1eqwrdeq  41732  mgmhmpropd  42110  issubmgm2  42115  isrnghmmul  42218  rngcsect  42305  rngcsectALTV  42317  ringcsect  42356  ringcsectALTV  42380  elbigo2  42671
 Copyright terms: Public domain W3C validator