Theorem pm5.32da 583

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

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 417	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 581	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rexbidva  3221  rexbida  3243  reubida  3306  reubidva  3307  rmobida  3311  cbvrexdva2  3370  rabbidva  3391  reuxfr1d  3665  mpteq12f  5116  reuhypd  5289  xpdifid  5998  funbrfv2b  6712  dffn5  6713  feqmptdf  6724  eqfnfv2  6795  fmptco  6883  dff13  7006  riotabidva  7128  mpoeq123dva  7223  mpoeq3dva  7226  opiota  7762  fnwelem  7831  suppssr  7871  mpoxopovel  7897  mpocurryd  7946  oeeui  8239  omabs  8285  qliftfun  8393  erovlem  8404  mapsnend  8608  xpcomco  8629  pw2f1olem  8643  elfi2  8912  cardval2  9454  dfac2b  9591  cflim3  9723  iundom2g  10001  fpwwe2lem7  10098  fpwwe2lem11  10102  ltexpi  10363  ordpipq  10403  axrrecex  10624  nnunb  11931  zrevaddcl  12067  qrevaddcl  12412  icoshft  12906  fznn  13025  preduz  13079  predfz  13082  fznnfl  13280  fz1isolem  13872  pfxeq  14106  pfxsuffeqwrdeq  14108  pfxsuff1eqwrdeq  14109  2swrd2eqwrdeq  14363  eqwrds3  14373  2shfti  14488  limsupgle  14883  ello12  14922  elo12  14933  isercoll  15073  sumeq2ii  15099  fsum2dlem  15174  prodeq2ii  15316  bitsmod  15836  bitscmp  15838  pwsle  16824  imasleval  16873  acsfiel  16984  ismon2  17064  isepi2  17071  oppcsect  17108  subsubc  17183  funcpropd  17230  fullpropd  17250  fucsect  17302  setcsect  17416  pltval3  17644  grpidpropd  17939  ismgmid  17942  gsumpropd2lem  17956  mhmpropd  18029  issubm2  18036  subgacs  18381  eqgid  18400  pgpfi2  18799  eqgabl  19024  iscyggen2  19069  cyggenod  19072  eldprd  19195  subgdmdprd  19225  dprd2d2  19235  ringpropd  19404  crngunit  19484  dvdsrpropd  19518  drngpropd  19598  issubrg3  19632  sdrgacs  19649  lsslss  19802  lsspropd  19858  lmhmpropd  19914  lbspropd  19940  znleval  20323  znunithash  20333  pjdm2  20477  islinds2  20579  aspval2  20662  bastop2  21695  elcls2  21775  neiptopreu  21834  maxlp  21848  restopn2  21878  iscnp3  21945  subbascn  21955  lmbr2  21960  kgencn  22257  kgencn2  22258  hauseqlcld  22347  txlm  22349  txkgen  22353  xkoptsub  22355  idqtop  22407  tgqtop  22413  qtopcld  22414  elmptrab  22528  flimopn  22676  fbflim  22677  fbflim2  22678  flimrest  22684  flffbas  22696  flftg  22697  cnflf  22703  cnflf2  22704  txflf  22707  isfcls  22710  fclsopn  22715  fclsbas  22722  fclsrest  22725  fcfnei  22736  cnfcf  22743  ptcmplem2  22754  tgphaus  22818  tsmssubm  22844  isucn2  22981  ismet2  23036  xblpnfps  23098  xblpnf  23099  blin  23124  blres  23134  elmopn2  23148  imasf1obl  23191  imasf1oxms  23192  prdsbl  23194  neibl  23204  metrest  23227  metcnp3  23243  metcnp  23244  metcnp2  23245  metcn  23246  txmetcnp  23250  txmetcn  23251  metuel2  23268  metucn  23274  ngppropd  23340  cnbl0  23476  cnblcld  23477  bl2ioo  23494  xrtgioo  23508  elcncf2  23592  cncfmet  23611  nmhmcn  23822  lmmbr  23959  lmmbr2  23960  iscfil2  23967  iscau2  23978  iscau3  23979  lmclim  24004  shft2rab  24209  sca2rab  24213  mbfeqalem1  24342  mbfmulc2lem  24348  mbfmax  24350  mbfposr  24353  mbfimaopnlem  24356  mbfaddlem  24361  mbfsup  24365  mbfinf  24366  i1fmullem  24395  i1fmulclem  24403  i1fres  24406  itg1climres  24415  mbfi1fseqlem4  24419  ibllem  24465  ellimc2  24577  ellimc3  24579  limcflf  24581  cnplimc  24587  cnlimc  24588  dvreslem  24609  ply1remlem  24863  fta1glem2  24867  ofmulrt  24978  plyremlem  25000  ulm2  25080  mcubic  25533  cubic2  25534  dvdsflsumcom  25873  fsumvma  25897  fsumvma2  25898  vmasum  25900  logfaclbnd  25906  dchrelbas2  25921  dchrelbas3  25922  dchrelbas4  25927  lgsquadlem1  26064  lgsquadlem2  26065  2lgslem1a  26075  colopp  26663  colhp  26664  umgr2v2enb1  27416  upgriswlk  27530  wspthsnwspthsnon  27802  elwwlks2on  27845  elwwlks2  27852  elwspths2spth  27853  isclwwlknx  27921  clwwlkn1  27926  clwwlkn2  27929  eupth2lems  28123  fusgr2wsp2nb  28219  numclwwlkqhash  28260  isblo2  28666  ubthlem1  28753  h2hlm  28863  pjpreeq  29281  elnlfn  29811  rmounid  30366  eqrrabd  30372  nfpconfp  30490  fmptcof2  30519  funcnvmpt  30529  suppiniseg  30545  ressupprn  30549  fpwrelmapffslem  30592  nndiffz1  30632  cntzun  30847  lindfpropd  31098  quslsm  31115  smatrcl  31268  zarcls  31346  rhmpreimacnlem  31356  ismntop  31496  itgeq12dv  31813  eulerpartlemgvv  31863  orvcgteel  31954  reprinrn  32118  reprdifc  32127  dfrdg2  33288  eqscut2  33562  broutsideof3  33978  isfne4b  34080  filnetlem4  34120  bj-elid6  34866  bj-imdirval3  34880  nlpineqsn  35106  uncf  35317  poimirlem23  35361  poimirlem26  35364  poimirlem27  35365  heicant  35373  cnambfre  35386  itg2gt0cn  35393  ftc1anclem5  35415  areacirclem5  35430  isdrngo3  35678  isidlc  35734  erim2  36352  prter3  36459  islshpsm  36557  islshpat  36594  lkrsc  36674  lfl1dim  36698  ldual1dim  36743  isat3  36884  glbconxN  36955  islln2  37088  islpln2  37113  islvol2  37157  cdlemg2cex  38168  diaglbN  38632  diblsmopel  38748  dihopelvalcpre  38825  xihopellsmN  38831  dihopellsm  38832  dihglbcpreN  38877  mapdval4N  39209  hdmapoc  39508  fsuppind  39785  fsuppssindlem2  39787  prjspreln0  39946  ellz1  40082  rmydioph  40329  rmxdioph  40331  expdiophlem1  40336  expdioph  40338  pw2f1ocnv  40352  dnwech  40366  rfovcnvf1od  41079  k0004lem3  41226  pm14.123b  41504  rfcnpre1  42022  rfcnpre2  42034  rfcnpre3  42036  rfcnpre4  42037  climreeq  42622  funbrafv2b  44084  dfafn5a  44085  isomushgr  44712  isomuspgr  44720  mgmhmpropd  44773  issubmgm2  44778  isrnghmmul  44885  rngcsect  44972  rngcsectALTV  44984  ringcsect  45023  ringcsectALTV  45047  elbigo2  45332  itsclc0b  45552  itscnhlinecirc02p  45565  pm5.32dav  45573  opndisj  45580  clddisj  45581