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 570
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 399 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 568 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  rexbida  3233  rexbidva  3235  reubida  3311  rmobida  3316  mpteq12f  4923  reuhypd  5090  xpdifid  5771  funbrfv2b  6459  dffn5  6460  feqmptdf  6470  eqfnfv2  6532  fmptco  6617  dff13  6734  riotabidva  6849  mpt2eq123dva  6944  mpt2eq3dva  6947  opiota  7459  fnwelem  7524  suppssr  7559  mpt2xopovel  7579  mpt2curryd  7628  oeeui  7917  omabs  7962  qliftfun  8065  erovlem  8077  xpcomco  8287  pw2f1olem  8301  elfi2  8557  cardval2  9098  dfac2b  9234  dfac2OLD  9236  cflim3  9367  iundom2g  9645  fpwwe2lem8  9742  fpwwe2lem12  9746  ltexpi  10007  ordpipq  10047  axrrecex  10267  nnunb  11553  zrevaddcl  11686  qrevaddcl  12027  icoshft  12513  fznn  12629  preduz  12683  predfz  12686  fznnfl  12883  fz1isolem  13460  swrdeq  13666  2swrdeqwrdeq  13675  2swrd1eqwrdeq  13676  2swrd2eqwrdeq  13919  eqwrds3  13927  2shfti  14041  limsupgle  14429  ello12  14468  elo12  14479  isercoll  14619  sumeq2ii  14644  fsum2dlem  14722  prodeq2ii  14862  bitsmod  15375  bitscmp  15377  pwsle  16355  imasleval  16404  acsfiel  16517  ismon2  16596  isepi2  16603  oppcsect  16640  subsubc  16715  funcpropd  16762  fullpropd  16782  fucsect  16834  setcsect  16941  pltval3  17170  grpidpropd  17464  ismgmid  17467  gsumpropd2lem  17476  mhmpropd  17544  issubm2  17551  subgacs  17829  eqgid  17846  pgpfi2  18220  eqgabl  18439  iscyggen2  18482  cyggenod  18485  eldprd  18603  subgdmdprd  18633  dprd2d2  18643  ringpropd  18782  crngunit  18862  dvdsrpropd  18896  drngpropd  18976  issubrg3  19010  lsslss  19166  lsspropd  19222  lmhmpropd  19278  lbspropd  19304  aspval2  19554  znleval  20108  znunithash  20118  pjdm2  20263  islinds2  20360  bastop2  21010  elcls2  21090  neiptopreu  21149  maxlp  21163  restopn2  21193  iscnp3  21260  subbascn  21270  lmbr2  21275  kgencn  21571  kgencn2  21572  hauseqlcld  21661  txlm  21663  txkgen  21667  xkoptsub  21669  idqtop  21721  tgqtop  21727  qtopcld  21728  elmptrab  21842  flimopn  21990  fbflim  21991  fbflim2  21992  flimrest  21998  flffbas  22010  flftg  22011  cnflf  22017  cnflf2  22018  txflf  22021  isfcls  22024  fclsopn  22029  fclsbas  22036  fclsrest  22039  fcfnei  22050  cnfcf  22057  ptcmplem2  22068  tgphaus  22131  tsmssubm  22157  isucn2  22294  ismet2  22349  xblpnfps  22411  xblpnf  22412  blin  22437  blres  22447  elmopn2  22461  imasf1obl  22504  imasf1oxms  22505  prdsbl  22507  neibl  22517  metrest  22540  metcnp3  22556  metcnp  22557  metcnp2  22558  metcn  22559  txmetcnp  22563  txmetcn  22564  metuel2  22581  metucn  22587  ngppropd  22652  cnbl0  22788  cnblcld  22789  bl2ioo  22806  xrtgioo  22820  elcncf2  22904  cncfmet  22922  nmhmcn  23130  lmmbr  23266  lmmbr2  23267  iscfil2  23274  iscau2  23285  iscau3  23286  lmclim  23311  shft2rab  23487  sca2rab  23491  mbfeqalem1  23620  mbfmulc2lem  23626  mbfmax  23628  mbfposr  23631  mbfimaopnlem  23634  mbfaddlem  23639  mbfsup  23643  mbfinf  23644  i1fmullem  23673  i1fmulclem  23681  i1fres  23684  itg1climres  23693  mbfi1fseqlem4  23697  ibllem  23743  ellimc2  23853  ellimc3  23855  limcflf  23857  cnplimc  23863  cnlimc  23864  dvreslem  23885  ply1remlem  24134  fta1glem2  24138  ofmulrt  24249  plyremlem  24271  ulm2  24351  mcubic  24786  cubic2  24787  dvdsflsumcom  25126  fsumvma  25150  fsumvma2  25151  vmasum  25153  logfaclbnd  25159  dchrelbas2  25174  dchrelbas3  25175  dchrelbas4  25180  lgsquadlem1  25317  lgsquadlem2  25318  2lgslem1a  25328  colopp  25873  colhp  25874  nbgrelOLD  26448  umgr2v2enb1  26648  upgriswlk  26763  wspthsnwspthsnon  27052  wspthsnwspthsnonOLD  27054  elwwlks2on  27098  elwwlks2  27106  elwspths2spth  27107  isclwwlknx  27182  clwwlkn1  27188  clwwlkn2  27191  eupth2lems  27409  fusgr2wsp2nb  27507  numclwwlkqhash  27553  isblo2  27964  ubthlem1  28052  h2hlm  28163  pjpreeq  28583  elnlfn  29113  reuxfr4d  29654  fmptcof2  29782  funcnvmpt  29793  fpwrelmapffslem  29832  nndiffz1  29873  smatrcl  30185  ismntop  30393  itgeq12dv  30711  eulerpartlemgvv  30761  orvcgteel  30852  reprinrn  31019  reprdifc  31028  dfrdg2  32019  broutsideof3  32552  isfne4b  32655  filnetlem4  32695  uncf  33699  poimirlem23  33743  poimirlem26  33746  poimirlem27  33747  heicant  33755  cnambfre  33768  itg2gt0cn  33775  ftc1anclem5  33799  areacirclem5  33814  isdrngo3  34067  isidlc  34123  prter3  34659  islshpsm  34758  islshpat  34795  lkrsc  34875  lfl1dim  34899  ldual1dim  34944  isat3  35085  glbconxN  35156  islln2  35289  islpln2  35314  islvol2  35358  cdlemg2cex  36370  diaglbN  36834  diblsmopel  36950  dihopelvalcpre  37027  xihopellsmN  37033  dihopellsm  37034  dihglbcpreN  37079  mapdval4N  37411  hdmapoc  37710  ellz1  37830  rmydioph  38080  rmxdioph  38082  expdiophlem1  38087  expdioph  38089  pw2f1ocnv  38103  dnwech  38117  sdrgacs  38270  rfovcnvf1od  38796  k0004lem3  38945  pm14.123b  39124  rfcnpre1  39670  rfcnpre2  39682  rfcnpre3  39684  rfcnpre4  39685  climreeq  40323  funbrafv2b  41746  dfafn5a  41747  pfxeq  41977  pfxsuffeqwrdeq  41979  pfxsuff1eqwrdeq  41980  mgmhmpropd  42351  issubmgm2  42356  isrnghmmul  42459  rngcsect  42546  rngcsectALTV  42558  ringcsect  42597  ringcsectALTV  42621  elbigo2  42912
  Copyright terms: Public domain W3C validator