Theorem pm5.32da 580

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 414	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 578	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  rexbidva  3177  rexbida  3270  cbvrexdva2OLD  3347  rmobidva  3392  reubidva  3393  rmobida  3403  reubida  3404  rabbidva  3440  rabbida  3459  reuxfr1d  3744  mpteq12da  5231  mpteq12f  5234  mpteq12dva  5235  reuhypd  5415  xpdifid  6163  funbrfv2b  6945  dffn5  6946  feqmptdf  6957  eqfnfv2  7028  fmptco  7121  dff13  7248  riotabidva  7379  mpoeq123dva  7477  mpoeq3dva  7480  opiota  8039  fnwelem  8111  suppssr  8175  mpoxopovel  8199  mpocurryd  8248  oeeui  8597  omabs  8645  eldifsucnn  8658  qliftfun  8791  erovlem  8802  mapsnend  9031  xpcomco  9057  pw2f1olem  9071  elfi2  9404  cardval2  9981  dfac2b  10120  cflim3  10252  iundom2g  10530  fpwwe2lem7  10627  fpwwe2lem11  10631  ltexpi  10892  ordpipq  10932  axrrecex  11153  nnunb  12463  zrevaddcl  12602  qrevaddcl  12950  icoshft  13445  fznn  13564  preduz  13618  predfz  13621  fznnfl  13822  fz1isolem  14417  pfxeq  14641  pfxsuffeqwrdeq  14643  pfxsuff1eqwrdeq  14644  2swrd2eqwrdeq  14899  eqwrds3  14907  2shfti  15022  limsupgle  15416  ello12  15455  elo12  15466  isercoll  15609  sumeq2ii  15634  fsum2dlem  15711  prodeq2ii  15852  bitsmod  16372  bitscmp  16374  pwsle  17433  imasleval  17482  acsfiel  17593  ismon2  17676  isepi2  17683  oppcsect  17720  subsubc  17798  funcpropd  17846  fullpropd  17866  fucsect  17920  setcsect  18034  pltval3  18287  grpidpropd  18576  ismgmid  18579  gsumpropd2lem  18593  mhmpropd  18673  issubm2  18680  subgacs  19034  eqgid  19053  eqg0subg  19066  pgpfi2  19466  eqgabl  19693  iscyggen2  19740  cyggenod  19743  eldprd  19865  subgdmdprd  19895  dprd2d2  19905  ringpropd  20091  crngunit  20180  dvdsrpropd  20218  drngpropd  20339  issubrg3  20379  sdrgacs  20404  lsslss  20559  lsspropd  20615  lmhmpropd  20671  lbspropd  20697  znleval  21093  znunithash  21103  pjdm2  21249  islinds2  21351  aspval2  21433  bastop2  22478  elcls2  22559  neiptopreu  22618  maxlp  22632  restopn2  22662  iscnp3  22729  subbascn  22739  lmbr2  22744  kgencn  23041  kgencn2  23042  hauseqlcld  23131  txlm  23133  txkgen  23137  xkoptsub  23139  idqtop  23191  tgqtop  23197  qtopcld  23198  elmptrab  23312  flimopn  23460  fbflim  23461  fbflim2  23462  flimrest  23468  flffbas  23480  flftg  23481  cnflf  23487  cnflf2  23488  txflf  23491  isfcls  23494  fclsopn  23499  fclsbas  23506  fclsrest  23509  fcfnei  23520  cnfcf  23527  ptcmplem2  23538  tgphaus  23602  tsmssubm  23628  isucn2  23765  ismet2  23820  xblpnfps  23882  xblpnf  23883  blin  23908  blres  23918  elmopn2  23932  imasf1obl  23978  imasf1oxms  23979  prdsbl  23981  neibl  23991  metrest  24014  metcnp3  24030  metcnp  24031  metcnp2  24032  metcn  24033  txmetcnp  24037  txmetcn  24038  metuel2  24055  metucn  24061  ngppropd  24127  cnbl0  24271  cnblcld  24272  bl2ioo  24289  xrtgioo  24303  elcncf2  24387  cncfmet  24406  nmhmcn  24617  lmmbr  24756  lmmbr2  24757  iscfil2  24764  iscau2  24775  iscau3  24776  lmclim  24801  shft2rab  25006  sca2rab  25010  mbfeqalem1  25139  mbfmulc2lem  25145  mbfmax  25147  mbfposr  25150  mbfimaopnlem  25153  mbfaddlem  25158  mbfsup  25162  mbfinf  25163  i1fmullem  25192  i1fmulclem  25201  i1fres  25204  itg1climres  25213  mbfi1fseqlem4  25217  ibllem  25263  ellimc2  25375  ellimc3  25377  limcflf  25379  cnplimc  25385  cnlimc  25386  dvreslem  25407  ply1remlem  25661  fta1glem2  25665  ofmulrt  25776  plyremlem  25798  ulm2  25878  mcubic  26331  cubic2  26332  dvdsflsumcom  26671  fsumvma  26695  fsumvma2  26696  vmasum  26698  logfaclbnd  26704  dchrelbas2  26719  dchrelbas3  26720  dchrelbas4  26725  lgsquadlem1  26862  lgsquadlem2  26863  2lgslem1a  26873  eqscut2  27286  colopp  27999  colhp  28000  umgr2v2enb1  28762  upgriswlk  28877  wspthsnwspthsnon  29149  elwwlks2on  29192  elwwlks2  29199  elwspths2spth  29200  isclwwlknx  29268  clwwlkn1  29273  clwwlkn2  29276  eupth2lems  29470  fusgr2wsp2nb  29566  numclwwlkqhash  29607  isblo2  30013  ubthlem1  30100  h2hlm  30210  pjpreeq  30628  elnlfn  31158  rmounid  31712  eqrrabd  31718  nfpconfp  31833  fmptcof2  31859  funcnvmpt  31869  suppiniseg  31885  ressupprn  31889  fpwrelmapffslem  31934  nndiffz1  31974  cntzun  32189  urpropd  32351  lindfpropd  32462  quslsm  32480  ghmqusker  32493  opprqus0g  32556  ressply1mon1p  32603  ply1degltel  32612  smatrcl  32713  zarcls  32791  rhmpreimacnlem  32801  ismntop  32943  itgeq12dv  33262  eulerpartlemgvv  33312  orvcgteel  33403  reprinrn  33567  reprdifc  33576  dfrdg2  34704  broutsideof3  35035  gg-dvcnp2  35111  gg-dvmulbr  35112  gg-dvcobr  35113  gg-cmvth  35118  gg-dvfsumle  35119  isfne4b  35163  filnetlem4  35203  bj-elid6  35988  bj-imdirval3  36002  nlpineqsn  36226  uncf  36404  poimirlem23  36448  poimirlem26  36451  poimirlem27  36452  heicant  36460  cnambfre  36473  itg2gt0cn  36480  ftc1anclem5  36502  areacirclem5  36517  isdrngo3  36764  isidlc  36820  erimeq2  37485  prter3  37689  islshpsm  37787  islshpat  37824  lkrsc  37904  lfl1dim  37928  ldual1dim  37973  isat3  38114  glbconxN  38186  islln2  38319  islpln2  38344  islvol2  38388  cdlemg2cex  39399  diaglbN  39863  diblsmopel  39979  dihopelvalcpre  40056  xihopellsmN  40062  dihopellsm  40063  dihglbcpreN  40108  mapdval4N  40440  hdmapoc  40739  fsuppind  41111  fsuppssindlem2  41113  prjspreln0  41294  ellz1  41437  rmydioph  41685  rmxdioph  41687  expdiophlem1  41692  expdioph  41694  pw2f1ocnv  41708  dnwech  41722  ordeldif  41940  ordeldifsucon  41941  ordeldif1o  41942  cantnfresb  42006  tfsconcat0i  42027  tfsconcatrev  42030  oadif1lem  42061  oadif1  42062  fzunt  42138  fzuntd  42139  fzunt1d  42140  fzuntgd  42141  rfovcnvf1od  42687  k0004lem3  42832  pm14.123b  43117  rfcnpre1  43635  rfcnpre2  43647  rfcnpre3  43649  rfcnpre4  43650  climreeq  44263  funbrafv2b  45801  dfafn5a  45802  isomushgr  46428  isomuspgr  46436  mgmhmpropd  46489  issubmgm2  46494  rngpropd  46607  isrnghmmul  46624  rngcsect  46779  rngcsectALTV  46791  ringcsect  46830  ringcsectALTV  46854  elbigo2  47139  itsclc0b  47359  itscnhlinecirc02p  47372  pm5.32dav  47380  opndisj  47436  clddisj  47437  lubeldm2d  47492  glbeldm2d  47493