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:  bian1d  580  rexbidva  3159  rexbida  3249  rmobidva  3355  reubidva  3356  rmobida  3365  reubida  3366  rabbidva  3395  rabbida  3415  reuxfr1d  3696  eqrrabd  4026  mpteq12da  5168  mpteq12f  5170  mpteq12dva  5171  reuhypd  5361  xpdifid  6132  funbrfv2b  6897  dffn5  6898  feqmptdf  6910  funcnvmpt  6949  eqfnfv2  6984  fmptco  7082  dff13  7209  riotabidva  7343  mpoeq123dva  7441  mpoeq3dva  7444  opiota  8012  fnwelem  8081  suppssr  8145  mpoxopovel  8170  mpocurryd  8219  oeeui  8538  omabs  8587  eldifsucnn  8600  qliftfun  8749  erovlem  8760  mapsnend  8983  xpcomco  9005  pw2f1olem  9019  elfi2  9327  cardval2  9915  dfac2b  10053  cflim3  10184  iundom2g  10462  fpwwe2lem7  10560  fpwwe2lem11  10564  ltexpi  10825  ordpipq  10865  axrrecex  11086  nnunb  12433  zrevaddcl  12572  qrevaddcl  12921  icoshft  13426  fznn  13546  preduz  13604  predfz  13607  fznnfl  13821  fz1isolem  14423  pfxeq  14658  pfxsuffeqwrdeq  14660  pfxsuff1eqwrdeq  14661  2swrd2eqwrdeq  14915  eqwrds3  14923  2shfti  15042  limsupgle  15439  ello12  15478  elo12  15489  isercoll  15630  sumeq2ii  15655  fsum2dlem  15732  prodeq2ii  15876  bitsmod  16405  bitscmp  16407  pwsle  17456  imasleval  17505  acsfiel  17620  ismon2  17701  isepi2  17708  oppcsect  17745  subsubc  17820  funcpropd  17869  fullpropd  17889  fucsect  17942  setcsect  18056  pltval3  18303  grpidpropd  18630  ismgmid  18633  gsumpropd2lem  18647  mgmhmpropd  18666  issubmgm2  18671  mhmpropd  18760  issubm2  18772  subgacs  19136  eqgid  19155  eqg0subg  19171  ghmqusker  19262  pgpfi2  19581  eqgabl  19809  iscyggen2  19856  cyggenod  19859  eldprd  19981  subgdmdprd  20011  dprd2d2  20021  rngpropd  20155  ringpropd  20269  crngunit  20358  dvdsrpropd  20396  isrnghmmul  20422  issubrg3  20577  rngcsect  20613  ringcsect  20647  drngpropd  20746  sdrgacs  20778  lsslss  20956  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  znleval  21534  znunithash  21544  pjdm2  21691  islinds2  21793  aspval2  21878  bastop2  22959  elcls2  23039  neiptopreu  23098  maxlp  23112  restopn2  23142  iscnp3  23209  subbascn  23219  lmbr2  23224  kgencn  23521  kgencn2  23522  hauseqlcld  23611  txlm  23613  txkgen  23617  xkoptsub  23619  idqtop  23671  tgqtop  23677  qtopcld  23678  elmptrab  23792  flimopn  23940  fbflim  23941  fbflim2  23942  flimrest  23948  flffbas  23960  flftg  23961  cnflf  23967  cnflf2  23968  txflf  23971  isfcls  23974  fclsopn  23979  fclsbas  23986  fclsrest  23989  fcfnei  24000  cnfcf  24007  ptcmplem2  24018  tgphaus  24082  tsmssubm  24108  isucn2  24243  ismet2  24298  xblpnfps  24360  xblpnf  24361  blin  24386  blres  24396  elmopn2  24410  imasf1obl  24453  imasf1oxms  24454  prdsbl  24456  neibl  24466  metrest  24489  metcnp3  24505  metcnp  24506  metcnp2  24507  metcn  24508  txmetcnp  24512  txmetcn  24513  metuel2  24530  metucn  24536  ngppropd  24602  cnbl0  24738  cnblcld  24739  bl2ioo  24757  xrtgioo  24772  elcncf2  24857  cncfmet  24876  nmhmcn  25087  lmmbr  25225  lmmbr2  25226  iscfil2  25233  iscau2  25244  iscau3  25245  lmclim  25270  shft2rab  25475  sca2rab  25479  mbfeqalem1  25608  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  mbfimaopnlem  25622  mbfaddlem  25627  mbfsup  25631  mbfinf  25632  i1fmullem  25661  i1fmulclem  25669  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  ibllem  25731  ellimc2  25844  ellimc3  25846  limcflf  25848  cnplimc  25854  cnlimc  25855  dvreslem  25876  dvcnp2  25887  dvmulbr  25906  dvcobr  25913  cmvth  25958  dvfsumle  25988  ply1remlem  26130  fta1glem2  26134  ofmulrt  26248  plyremlem  26270  ulm2  26350  mcubic  26811  cubic2  26812  dvdsflsumcom  27151  fsumvma  27176  fsumvma2  27177  vmasum  27179  logfaclbnd  27185  dchrelbas2  27200  dchrelbas3  27201  dchrelbas4  27206  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a  27354  eqcuts2  27778  colopp  28837  colhp  28838  umgr2v2enb1  29595  upgriswlk  29709  wspthsnwspthsnon  29984  elwwlks2on  30029  elwwlks2  30037  elwspths2spth  30038  isclwwlknx  30106  clwwlkn1  30111  clwwlkn2  30114  eupth2lems  30308  fusgr2wsp2nb  30404  numclwwlkqhash  30445  isblo2  30854  ubthlem1  30941  h2hlm  31051  pjpreeq  31469  elnlfn  31999  rmounid  32564  nfpconfp  32705  fmptcof2  32730  fdifsupp  32758  suppiniseg  32759  ressupprn  32763  fpwrelmapffslem  32805  nndiffz1  32859  cntzun  33140  cntrval2  33232  urpropd  33292  lindfpropd  33442  quslsm  33465  opprqus0g  33550  ressply1mon1p  33628  ply1degltel  33654  ply1degleel  33655  algextdeglem6  33866  smatrcl  33940  zarcls  34018  rhmpreimacnlem  34028  ismntop  34170  itgeq12dv  34470  eulerpartlemgvv  34520  orvcgteel  34612  reprinrn  34762  reprdifc  34771  dfrdg2  35975  broutsideof3  36308  isfne4b  36523  filnetlem4  36563  bj-elid6  37484  bj-imdirval3  37498  nlpineqsn  37724  uncf  37920  poimirlem23  37964  poimirlem26  37967  poimirlem27  37968  heicant  37976  cnambfre  37989  itg2gt0cn  37996  ftc1anclem5  38018  areacirclem5  38033  isdrngo3  38280  isidlc  38336  erimeq2  39084  prter3  39328  islshpsm  39426  islshpat  39463  lkrsc  39543  lfl1dim  39567  ldual1dim  39612  isat3  39753  glbconxN  39824  islln2  39957  islpln2  39982  islvol2  40026  cdlemg2cex  41037  diaglbN  41501  diblsmopel  41617  dihopelvalcpre  41694  xihopellsmN  41700  dihopellsm  41701  dihglbcpreN  41746  mapdval4N  42078  hdmapoc  42377  eluzp1  42739  fsuppind  43023  fsuppssindlem2  43025  prjspreln0  43042  ellz1  43199  rmydioph  43442  rmxdioph  43444  expdiophlem1  43449  expdioph  43451  pw2f1ocnv  43465  dnwech  43476  ordeldif  43686  ordeldifsucon  43687  ordeldif1o  43688  cantnfresb  43752  tfsconcat0i  43773  tfsconcatrev  43776  oadif1lem  43807  oadif1  43808  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  rfovcnvf1od  44431  k0004lem3  44576  pm14.123b  44853  rfcnpre1  45450  rfcnpre2  45462  rfcnpre3  45464  rfcnpre4  45465  climreeq  46043  funbrafv2b  47607  dfafn5a  47608  isuspgrim0  48370  gricushgr  48393  isubgrgrim  48405  rngcsectALTV  48751  ringcsectALTV  48785  elbigo2  49028  itsclc0b  49248  itscnhlinecirc02p  49261  pm5.32dav  49269  reuxfr1dd  49282  opndisj  49378  clddisj  49379  lubeldm2d  49433  glbeldm2d  49434  sectpropdlem  49511  uppropd  49656  initopropd  49718  termopropd  49719