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

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  rexbidva  3176  rexbida  3269  cbvrexdva2OLD  3346  rmobidva  3391  reubidva  3392  rmobida  3402  reubida  3403  rabbidva  3439  rabbida  3458  reuxfr1d  3746  mpteq12da  5233  mpteq12f  5236  mpteq12dva  5237  reuhypd  5417  xpdifid  6167  funbrfv2b  6949  dffn5  6950  feqmptdf  6962  eqfnfv2  7033  fmptco  7126  dff13  7253  riotabidva  7384  mpoeq123dva  7482  mpoeq3dva  7485  opiota  8044  fnwelem  8116  suppssr  8180  mpoxopovel  8204  mpocurryd  8253  oeeui  8601  omabs  8649  eldifsucnn  8662  qliftfun  8795  erovlem  8806  mapsnend  9035  xpcomco  9061  pw2f1olem  9075  elfi2  9408  cardval2  9985  dfac2b  10124  cflim3  10256  iundom2g  10534  fpwwe2lem7  10631  fpwwe2lem11  10635  ltexpi  10896  ordpipq  10936  axrrecex  11157  nnunb  12467  zrevaddcl  12606  qrevaddcl  12954  icoshft  13449  fznn  13568  preduz  13622  predfz  13625  fznnfl  13826  fz1isolem  14421  pfxeq  14645  pfxsuffeqwrdeq  14647  pfxsuff1eqwrdeq  14648  2swrd2eqwrdeq  14903  eqwrds3  14911  2shfti  15026  limsupgle  15420  ello12  15459  elo12  15470  isercoll  15613  sumeq2ii  15638  fsum2dlem  15715  prodeq2ii  15856  bitsmod  16376  bitscmp  16378  pwsle  17437  imasleval  17486  acsfiel  17597  ismon2  17680  isepi2  17687  oppcsect  17724  subsubc  17802  funcpropd  17850  fullpropd  17870  fucsect  17924  setcsect  18038  pltval3  18291  grpidpropd  18580  ismgmid  18583  gsumpropd2lem  18597  mhmpropd  18677  issubm2  18684  subgacs  19040  eqgid  19059  eqg0subg  19072  pgpfi2  19473  eqgabl  19701  iscyggen2  19748  cyggenod  19751  eldprd  19873  subgdmdprd  19903  dprd2d2  19913  ringpropd  20101  crngunit  20191  dvdsrpropd  20229  issubrg3  20346  drngpropd  20393  sdrgacs  20416  lsslss  20571  lsspropd  20627  lmhmpropd  20683  lbspropd  20709  znleval  21109  znunithash  21119  pjdm2  21265  islinds2  21367  aspval2  21451  bastop2  22496  elcls2  22577  neiptopreu  22636  maxlp  22650  restopn2  22680  iscnp3  22747  subbascn  22757  lmbr2  22762  kgencn  23059  kgencn2  23060  hauseqlcld  23149  txlm  23151  txkgen  23155  xkoptsub  23157  idqtop  23209  tgqtop  23215  qtopcld  23216  elmptrab  23330  flimopn  23478  fbflim  23479  fbflim2  23480  flimrest  23486  flffbas  23498  flftg  23499  cnflf  23505  cnflf2  23506  txflf  23509  isfcls  23512  fclsopn  23517  fclsbas  23524  fclsrest  23527  fcfnei  23538  cnfcf  23545  ptcmplem2  23556  tgphaus  23620  tsmssubm  23646  isucn2  23783  ismet2  23838  xblpnfps  23900  xblpnf  23901  blin  23926  blres  23936  elmopn2  23950  imasf1obl  23996  imasf1oxms  23997  prdsbl  23999  neibl  24009  metrest  24032  metcnp3  24048  metcnp  24049  metcnp2  24050  metcn  24051  txmetcnp  24055  txmetcn  24056  metuel2  24073  metucn  24079  ngppropd  24145  cnbl0  24289  cnblcld  24290  bl2ioo  24307  xrtgioo  24321  elcncf2  24405  cncfmet  24424  nmhmcn  24635  lmmbr  24774  lmmbr2  24775  iscfil2  24782  iscau2  24793  iscau3  24794  lmclim  24819  shft2rab  25024  sca2rab  25028  mbfeqalem1  25157  mbfmulc2lem  25163  mbfmax  25165  mbfposr  25168  mbfimaopnlem  25171  mbfaddlem  25176  mbfsup  25180  mbfinf  25181  i1fmullem  25210  i1fmulclem  25219  i1fres  25222  itg1climres  25231  mbfi1fseqlem4  25235  ibllem  25281  ellimc2  25393  ellimc3  25395  limcflf  25397  cnplimc  25403  cnlimc  25404  dvreslem  25425  ply1remlem  25679  fta1glem2  25683  ofmulrt  25794  plyremlem  25816  ulm2  25896  mcubic  26349  cubic2  26350  dvdsflsumcom  26689  fsumvma  26713  fsumvma2  26714  vmasum  26716  logfaclbnd  26722  dchrelbas2  26737  dchrelbas3  26738  dchrelbas4  26743  lgsquadlem1  26880  lgsquadlem2  26881  2lgslem1a  26891  eqscut2  27304  colopp  28017  colhp  28018  umgr2v2enb1  28780  upgriswlk  28895  wspthsnwspthsnon  29167  elwwlks2on  29210  elwwlks2  29217  elwspths2spth  29218  isclwwlknx  29286  clwwlkn1  29291  clwwlkn2  29294  eupth2lems  29488  fusgr2wsp2nb  29584  numclwwlkqhash  29625  isblo2  30031  ubthlem1  30118  h2hlm  30228  pjpreeq  30646  elnlfn  31176  rmounid  31730  eqrrabd  31736  nfpconfp  31851  fmptcof2  31877  funcnvmpt  31887  suppiniseg  31903  ressupprn  31907  fpwrelmapffslem  31952  nndiffz1  31992  cntzun  32207  urpropd  32373  lindfpropd  32493  quslsm  32511  ghmqusker  32527  opprqus0g  32599  ressply1mon1p  32652  ply1degltel  32661  smatrcl  32771  zarcls  32849  rhmpreimacnlem  32859  ismntop  33001  itgeq12dv  33320  eulerpartlemgvv  33370  orvcgteel  33461  reprinrn  33625  reprdifc  33634  dfrdg2  34762  broutsideof3  35093  gg-dvcnp2  35169  gg-dvmulbr  35170  gg-dvcobr  35171  gg-cmvth  35176  gg-dvfsumle  35177  isfne4b  35221  filnetlem4  35261  bj-elid6  36046  bj-imdirval3  36060  nlpineqsn  36284  uncf  36462  poimirlem23  36506  poimirlem26  36509  poimirlem27  36510  heicant  36518  cnambfre  36531  itg2gt0cn  36538  ftc1anclem5  36560  areacirclem5  36575  isdrngo3  36822  isidlc  36878  erimeq2  37543  prter3  37747  islshpsm  37845  islshpat  37882  lkrsc  37962  lfl1dim  37986  ldual1dim  38031  isat3  38172  glbconxN  38244  islln2  38377  islpln2  38402  islvol2  38446  cdlemg2cex  39457  diaglbN  39921  diblsmopel  40037  dihopelvalcpre  40114  xihopellsmN  40120  dihopellsm  40121  dihglbcpreN  40166  mapdval4N  40498  hdmapoc  40797  fsuppind  41164  fsuppssindlem2  41166  prjspreln0  41352  ellz1  41495  rmydioph  41743  rmxdioph  41745  expdiophlem1  41750  expdioph  41752  pw2f1ocnv  41766  dnwech  41780  ordeldif  41998  ordeldifsucon  41999  ordeldif1o  42000  cantnfresb  42064  tfsconcat0i  42085  tfsconcatrev  42088  oadif1lem  42119  oadif1  42120  fzunt  42196  fzuntd  42197  fzunt1d  42198  fzuntgd  42199  rfovcnvf1od  42745  k0004lem3  42890  pm14.123b  43175  rfcnpre1  43693  rfcnpre2  43705  rfcnpre3  43707  rfcnpre4  43708  climreeq  44319  funbrafv2b  45857  dfafn5a  45858  isomushgr  46484  isomuspgr  46492  mgmhmpropd  46545  issubmgm2  46550  rngpropd  46663  isrnghmmul  46681  rngcsect  46868  rngcsectALTV  46880  ringcsect  46919  ringcsectALTV  46943  elbigo2  47228  itsclc0b  47448  itscnhlinecirc02p  47461  pm5.32dav  47469  opndisj  47525  clddisj  47526  lubeldm2d  47581  glbeldm2d  47582