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

Theorem pm5.32da 579
Description: Distribution of implication over biconditional (deduction form). (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 413 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 577 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  rexbidva  3293  rexbida  3315  reubida  3385  reubidva  3386  rmobida  3390  cbvrexdva2  3455  rabbidva  3476  reuxfr1d  3738  mpteq12f  5140  reuhypd  5310  xpdifid  6018  funbrfv2b  6716  dffn5  6717  feqmptdf  6728  eqfnfv2  6795  fmptco  6883  dff13  7004  riotabidva  7122  mpoeq123dva  7217  mpoeq3dva  7220  opiota  7746  fnwelem  7814  suppssr  7850  mpoxopovel  7875  mpocurryd  7924  oeeui  8217  omabs  8263  qliftfun  8371  erovlem  8382  mapsnend  8576  xpcomco  8595  pw2f1olem  8609  elfi2  8866  cardval2  9408  dfac2b  9544  cflim3  9672  iundom2g  9950  fpwwe2lem8  10047  fpwwe2lem12  10051  ltexpi  10312  ordpipq  10352  axrrecex  10573  nnunb  11881  zrevaddcl  12015  qrevaddcl  12358  icoshft  12847  fznn  12963  preduz  13017  predfz  13020  fznnfl  13218  fz1isolem  13807  pfxeq  14046  pfxsuffeqwrdeq  14048  pfxsuff1eqwrdeq  14049  2swrd2eqwrdeq  14303  eqwrds3  14313  2shfti  14427  limsupgle  14822  ello12  14861  elo12  14872  isercoll  15012  sumeq2ii  15038  fsum2dlem  15113  prodeq2ii  15255  bitsmod  15773  bitscmp  15775  pwsle  16753  imasleval  16802  acsfiel  16913  ismon2  16992  isepi2  16999  oppcsect  17036  subsubc  17111  funcpropd  17158  fullpropd  17178  fucsect  17230  setcsect  17337  pltval3  17565  grpidpropd  17860  ismgmid  17863  gsumpropd2lem  17877  mhmpropd  17950  issubm2  17957  subgacs  18251  eqgid  18270  pgpfi2  18660  eqgabl  18884  iscyggen2  18929  cyggenod  18932  eldprd  19055  subgdmdprd  19085  dprd2d2  19095  ringpropd  19261  crngunit  19341  dvdsrpropd  19375  drngpropd  19458  issubrg3  19492  sdrgacs  19509  lsslss  19662  lsspropd  19718  lmhmpropd  19774  lbspropd  19800  aspval2  20055  znleval  20629  znunithash  20639  pjdm2  20783  islinds2  20885  bastop2  21530  elcls2  21610  neiptopreu  21669  maxlp  21683  restopn2  21713  iscnp3  21780  subbascn  21790  lmbr2  21795  kgencn  22092  kgencn2  22093  hauseqlcld  22182  txlm  22184  txkgen  22188  xkoptsub  22190  idqtop  22242  tgqtop  22248  qtopcld  22249  elmptrab  22363  flimopn  22511  fbflim  22512  fbflim2  22513  flimrest  22519  flffbas  22531  flftg  22532  cnflf  22538  cnflf2  22539  txflf  22542  isfcls  22545  fclsopn  22550  fclsbas  22557  fclsrest  22560  fcfnei  22571  cnfcf  22578  ptcmplem2  22589  tgphaus  22652  tsmssubm  22678  isucn2  22815  ismet2  22870  xblpnfps  22932  xblpnf  22933  blin  22958  blres  22968  elmopn2  22982  imasf1obl  23025  imasf1oxms  23026  prdsbl  23028  neibl  23038  metrest  23061  metcnp3  23077  metcnp  23078  metcnp2  23079  metcn  23080  txmetcnp  23084  txmetcn  23085  metuel2  23102  metucn  23108  ngppropd  23173  cnbl0  23309  cnblcld  23310  bl2ioo  23327  xrtgioo  23341  elcncf2  23425  cncfmet  23443  nmhmcn  23651  lmmbr  23788  lmmbr2  23789  iscfil2  23796  iscau2  23807  iscau3  23808  lmclim  23833  shft2rab  24036  sca2rab  24040  mbfeqalem1  24169  mbfmulc2lem  24175  mbfmax  24177  mbfposr  24180  mbfimaopnlem  24183  mbfaddlem  24188  mbfsup  24192  mbfinf  24193  i1fmullem  24222  i1fmulclem  24230  i1fres  24233  itg1climres  24242  mbfi1fseqlem4  24246  ibllem  24292  ellimc2  24402  ellimc3  24404  limcflf  24406  cnplimc  24412  cnlimc  24413  dvreslem  24434  ply1remlem  24683  fta1glem2  24687  ofmulrt  24798  plyremlem  24820  ulm2  24900  mcubic  25352  cubic2  25353  dvdsflsumcom  25692  fsumvma  25716  fsumvma2  25717  vmasum  25719  logfaclbnd  25725  dchrelbas2  25740  dchrelbas3  25741  dchrelbas4  25746  lgsquadlem1  25883  lgsquadlem2  25884  2lgslem1a  25894  colopp  26482  colhp  26483  umgr2v2enb1  27235  upgriswlk  27349  wspthsnwspthsnon  27622  elwwlks2on  27665  elwwlks2  27672  elwspths2spth  27673  isclwwlknx  27741  clwwlkn1  27746  clwwlkn2  27749  eupth2lems  27944  fusgr2wsp2nb  28040  numclwwlkqhash  28081  isblo2  28487  ubthlem1  28574  h2hlm  28684  pjpreeq  29102  elnlfn  29632  rmounid  30186  nfpconfp  30305  fmptcof2  30330  funcnvmpt  30340  fpwrelmapffslem  30394  nndiffz1  30435  cntzun  30622  lindfpropd  30869  smatrcl  30960  ismntop  31166  itgeq12dv  31483  eulerpartlemgvv  31533  orvcgteel  31624  reprinrn  31788  reprdifc  31797  dfrdg2  32937  broutsideof3  33484  isfne4b  33586  filnetlem4  33626  bj-elid6  34354  bj-imdirval3  34366  bj-imdirid  34367  nlpineqsn  34571  uncf  34752  poimirlem23  34796  poimirlem26  34799  poimirlem27  34800  heicant  34808  cnambfre  34821  itg2gt0cn  34828  ftc1anclem5  34852  areacirclem5  34867  isdrngo3  35118  isidlc  35174  erim2  35791  prter3  35898  islshpsm  35996  islshpat  36033  lkrsc  36113  lfl1dim  36137  ldual1dim  36182  isat3  36323  glbconxN  36394  islln2  36527  islpln2  36552  islvol2  36596  cdlemg2cex  37607  diaglbN  38071  diblsmopel  38187  dihopelvalcpre  38264  xihopellsmN  38270  dihopellsm  38271  dihglbcpreN  38316  mapdval4N  38648  hdmapoc  38947  prjspreln0  39137  ellz1  39242  rmydioph  39489  rmxdioph  39491  expdiophlem1  39496  expdioph  39498  pw2f1ocnv  39512  dnwech  39526  rfovcnvf1od  40228  k0004lem3  40377  pm14.123b  40635  rfcnpre1  41153  rfcnpre2  41165  rfcnpre3  41167  rfcnpre4  41168  climreeq  41770  funbrafv2b  43235  dfafn5a  43236  isomushgr  43868  isomuspgr  43876  mgmhmpropd  43929  issubmgm2  43934  isrnghmmul  44092  rngcsect  44179  rngcsectALTV  44191  ringcsect  44230  ringcsectALTV  44254  elbigo2  44540  itsclc0b  44687  itscnhlinecirc02p  44700
  Copyright terms: Public domain W3C validator