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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rexbidva  3154  rexbida  3244  rmobidva  3359  reubidva  3360  rmobida  3369  reubida  3370  rabbidva  3401  rabbida  3421  reuxfr1d  3709  eqrrabd  4036  mpteq12da  5174  mpteq12f  5176  mpteq12dva  5177  reuhypd  5357  xpdifid  6115  funbrfv2b  6879  dffn5  6880  feqmptdf  6892  eqfnfv2  6965  fmptco  7062  dff13  7188  riotabidva  7322  mpoeq123dva  7420  mpoeq3dva  7423  opiota  7991  fnwelem  8061  suppssr  8125  mpoxopovel  8150  mpocurryd  8199  oeeui  8517  omabs  8566  eldifsucnn  8579  qliftfun  8726  erovlem  8737  mapsnend  8958  xpcomco  8980  pw2f1olem  8994  elfi2  9298  cardval2  9881  dfac2b  10019  cflim3  10150  iundom2g  10428  fpwwe2lem7  10525  fpwwe2lem11  10529  ltexpi  10790  ordpipq  10830  axrrecex  11051  nnunb  12374  zrevaddcl  12514  qrevaddcl  12866  icoshft  13370  fznn  13489  preduz  13547  predfz  13550  fznnfl  13763  fz1isolem  14365  pfxeq  14600  pfxsuffeqwrdeq  14602  pfxsuff1eqwrdeq  14603  2swrd2eqwrdeq  14857  eqwrds3  14865  2shfti  14984  limsupgle  15381  ello12  15420  elo12  15431  isercoll  15572  sumeq2ii  15597  fsum2dlem  15674  prodeq2ii  15815  bitsmod  16344  bitscmp  16346  pwsle  17393  imasleval  17442  acsfiel  17557  ismon2  17638  isepi2  17645  oppcsect  17682  subsubc  17757  funcpropd  17806  fullpropd  17826  fucsect  17879  setcsect  17993  pltval3  18240  grpidpropd  18567  ismgmid  18570  gsumpropd2lem  18584  mgmhmpropd  18603  issubmgm2  18608  mhmpropd  18697  issubm2  18709  subgacs  19071  eqgid  19090  eqg0subg  19106  ghmqusker  19197  pgpfi2  19516  eqgabl  19744  iscyggen2  19791  cyggenod  19794  eldprd  19916  subgdmdprd  19946  dprd2d2  19956  rngpropd  20090  ringpropd  20204  crngunit  20294  dvdsrpropd  20332  isrnghmmul  20358  issubrg3  20513  rngcsect  20549  ringcsect  20583  drngpropd  20682  sdrgacs  20714  lsslss  20892  lsspropd  20949  lmhmpropd  21005  lbspropd  21031  znleval  21489  znunithash  21499  pjdm2  21646  islinds2  21748  aspval2  21833  bastop2  22907  elcls2  22987  neiptopreu  23046  maxlp  23060  restopn2  23090  iscnp3  23157  subbascn  23167  lmbr2  23172  kgencn  23469  kgencn2  23470  hauseqlcld  23559  txlm  23561  txkgen  23565  xkoptsub  23567  idqtop  23619  tgqtop  23625  qtopcld  23626  elmptrab  23740  flimopn  23888  fbflim  23889  fbflim2  23890  flimrest  23896  flffbas  23908  flftg  23909  cnflf  23915  cnflf2  23916  txflf  23919  isfcls  23922  fclsopn  23927  fclsbas  23934  fclsrest  23937  fcfnei  23948  cnfcf  23955  ptcmplem2  23966  tgphaus  24030  tsmssubm  24056  isucn2  24191  ismet2  24246  xblpnfps  24308  xblpnf  24309  blin  24334  blres  24344  elmopn2  24358  imasf1obl  24401  imasf1oxms  24402  prdsbl  24404  neibl  24414  metrest  24437  metcnp3  24453  metcnp  24454  metcnp2  24455  metcn  24456  txmetcnp  24460  txmetcn  24461  metuel2  24478  metucn  24484  ngppropd  24550  cnbl0  24686  cnblcld  24687  bl2ioo  24705  xrtgioo  24720  elcncf2  24808  cncfmet  24827  nmhmcn  25045  lmmbr  25183  lmmbr2  25184  iscfil2  25191  iscau2  25202  iscau3  25203  lmclim  25228  shft2rab  25434  sca2rab  25438  mbfeqalem1  25567  mbfmulc2lem  25573  mbfmax  25575  mbfposr  25578  mbfimaopnlem  25581  mbfaddlem  25586  mbfsup  25590  mbfinf  25591  i1fmullem  25620  i1fmulclem  25628  i1fres  25631  itg1climres  25640  mbfi1fseqlem4  25644  ibllem  25690  ellimc2  25803  ellimc3  25805  limcflf  25807  cnplimc  25813  cnlimc  25814  dvreslem  25835  dvcnp2  25846  dvmulbr  25866  dvcobr  25874  cmvth  25920  dvfsumle  25951  ply1remlem  26095  fta1glem2  26099  ofmulrt  26214  plyremlem  26237  ulm2  26319  mcubic  26782  cubic2  26783  dvdsflsumcom  27123  fsumvma  27149  fsumvma2  27150  vmasum  27152  logfaclbnd  27158  dchrelbas2  27173  dchrelbas3  27174  dchrelbas4  27179  lgsquadlem1  27316  lgsquadlem2  27317  2lgslem1a  27327  eqscut2  27745  colopp  28745  colhp  28746  umgr2v2enb1  29503  upgriswlk  29617  wspthsnwspthsnon  29892  elwwlks2on  29935  elwwlks2  29942  elwspths2spth  29943  isclwwlknx  30011  clwwlkn1  30016  clwwlkn2  30019  eupth2lems  30213  fusgr2wsp2nb  30309  numclwwlkqhash  30350  isblo2  30758  ubthlem1  30845  h2hlm  30955  pjpreeq  31373  elnlfn  31903  rmounid  32469  nfpconfp  32609  fmptcof2  32634  funcnvmpt  32644  fdifsupp  32661  suppiniseg  32662  ressupprn  32666  fpwrelmapffslem  32710  nndiffz1  32764  cntzun  33043  cntrval2  33135  urpropd  33194  lindfpropd  33342  quslsm  33365  opprqus0g  33450  ressply1mon1p  33526  ply1degltel  33550  ply1degleel  33551  algextdeglem6  33730  smatrcl  33804  zarcls  33882  rhmpreimacnlem  33892  ismntop  34034  itgeq12dv  34334  eulerpartlemgvv  34384  orvcgteel  34476  reprinrn  34626  reprdifc  34635  dfrdg2  35828  broutsideof3  36159  isfne4b  36374  filnetlem4  36414  bj-elid6  37203  bj-imdirval3  37217  nlpineqsn  37441  uncf  37638  poimirlem23  37682  poimirlem26  37685  poimirlem27  37686  heicant  37694  cnambfre  37707  itg2gt0cn  37714  ftc1anclem5  37736  areacirclem5  37751  isdrngo3  37998  isidlc  38054  erimeq2  38715  prter3  38920  islshpsm  39018  islshpat  39055  lkrsc  39135  lfl1dim  39159  ldual1dim  39204  isat3  39345  glbconxN  39416  islln2  39549  islpln2  39574  islvol2  39618  cdlemg2cex  40629  diaglbN  41093  diblsmopel  41209  dihopelvalcpre  41286  xihopellsmN  41292  dihopellsm  41293  dihglbcpreN  41338  mapdval4N  41670  hdmapoc  41969  eluzp1  42339  fsuppind  42622  fsuppssindlem2  42624  prjspreln0  42641  ellz1  42799  rmydioph  43046  rmxdioph  43048  expdiophlem1  43053  expdioph  43055  pw2f1ocnv  43069  dnwech  43080  ordeldif  43290  ordeldifsucon  43291  ordeldif1o  43292  cantnfresb  43356  tfsconcat0i  43377  tfsconcatrev  43380  oadif1lem  43411  oadif1  43412  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  rfovcnvf1od  44036  k0004lem3  44181  pm14.123b  44458  rfcnpre1  45055  rfcnpre2  45067  rfcnpre3  45069  rfcnpre4  45070  climreeq  45652  funbrafv2b  47189  dfafn5a  47190  isuspgrim0  47924  gricushgr  47947  isubgrgrim  47959  rngcsectALTV  48305  ringcsectALTV  48339  elbigo2  48583  itsclc0b  48803  itscnhlinecirc02p  48816  pm5.32dav  48824  reuxfr1dd  48837  opndisj  48933  clddisj  48934  lubeldm2d  48988  glbeldm2d  48989  sectpropdlem  49067  uppropd  49212  initopropd  49274  termopropd  49275