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  3151  rexbida  3241  cbvrexdva2OLD  3314  rmobidva  3360  reubidva  3361  rmobida  3370  reubida  3371  rabbidva  3403  rabbida  3423  reuxfr1d  3712  eqrrabd  4039  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  reuhypd  5361  xpdifid  6121  funbrfv2b  6884  dffn5  6885  feqmptdf  6897  eqfnfv2  6970  fmptco  7067  dff13  7195  riotabidva  7329  mpoeq123dva  7427  mpoeq3dva  7430  opiota  8001  fnwelem  8071  suppssr  8135  mpoxopovel  8160  mpocurryd  8209  oeeui  8527  omabs  8576  eldifsucnn  8589  qliftfun  8736  erovlem  8747  mapsnend  8968  xpcomco  8991  pw2f1olem  9005  elfi2  9323  cardval2  9906  dfac2b  10044  cflim3  10175  iundom2g  10453  fpwwe2lem7  10550  fpwwe2lem11  10554  ltexpi  10815  ordpipq  10855  axrrecex  11076  nnunb  12398  zrevaddcl  12538  qrevaddcl  12890  icoshft  13394  fznn  13513  preduz  13571  predfz  13574  fznnfl  13784  fz1isolem  14386  pfxeq  14620  pfxsuffeqwrdeq  14622  pfxsuff1eqwrdeq  14623  2swrd2eqwrdeq  14878  eqwrds3  14886  2shfti  15005  limsupgle  15402  ello12  15441  elo12  15452  isercoll  15593  sumeq2ii  15618  fsum2dlem  15695  prodeq2ii  15836  bitsmod  16365  bitscmp  16367  pwsle  17414  imasleval  17463  acsfiel  17578  ismon2  17659  isepi2  17666  oppcsect  17703  subsubc  17778  funcpropd  17827  fullpropd  17847  fucsect  17900  setcsect  18014  pltval3  18261  grpidpropd  18554  ismgmid  18557  gsumpropd2lem  18571  mgmhmpropd  18590  issubmgm2  18595  mhmpropd  18684  issubm2  18696  subgacs  19058  eqgid  19077  eqg0subg  19093  ghmqusker  19184  pgpfi2  19503  eqgabl  19731  iscyggen2  19778  cyggenod  19781  eldprd  19903  subgdmdprd  19933  dprd2d2  19943  rngpropd  20077  ringpropd  20191  crngunit  20281  dvdsrpropd  20319  isrnghmmul  20345  issubrg3  20503  rngcsect  20539  ringcsect  20573  drngpropd  20672  sdrgacs  20704  lsslss  20882  lsspropd  20939  lmhmpropd  20995  lbspropd  21021  znleval  21479  znunithash  21489  pjdm2  21636  islinds2  21738  aspval2  21823  bastop2  22897  elcls2  22977  neiptopreu  23036  maxlp  23050  restopn2  23080  iscnp3  23147  subbascn  23157  lmbr2  23162  kgencn  23459  kgencn2  23460  hauseqlcld  23549  txlm  23551  txkgen  23555  xkoptsub  23557  idqtop  23609  tgqtop  23615  qtopcld  23616  elmptrab  23730  flimopn  23878  fbflim  23879  fbflim2  23880  flimrest  23886  flffbas  23898  flftg  23899  cnflf  23905  cnflf2  23906  txflf  23909  isfcls  23912  fclsopn  23917  fclsbas  23924  fclsrest  23927  fcfnei  23938  cnfcf  23945  ptcmplem2  23956  tgphaus  24020  tsmssubm  24046  isucn2  24182  ismet2  24237  xblpnfps  24299  xblpnf  24300  blin  24325  blres  24335  elmopn2  24349  imasf1obl  24392  imasf1oxms  24393  prdsbl  24395  neibl  24405  metrest  24428  metcnp3  24444  metcnp  24445  metcnp2  24446  metcn  24447  txmetcnp  24451  txmetcn  24452  metuel2  24469  metucn  24475  ngppropd  24541  cnbl0  24677  cnblcld  24678  bl2ioo  24696  xrtgioo  24711  elcncf2  24799  cncfmet  24818  nmhmcn  25036  lmmbr  25174  lmmbr2  25175  iscfil2  25182  iscau2  25193  iscau3  25194  lmclim  25219  shft2rab  25425  sca2rab  25429  mbfeqalem1  25558  mbfmulc2lem  25564  mbfmax  25566  mbfposr  25569  mbfimaopnlem  25572  mbfaddlem  25577  mbfsup  25581  mbfinf  25582  i1fmullem  25611  i1fmulclem  25619  i1fres  25622  itg1climres  25631  mbfi1fseqlem4  25635  ibllem  25681  ellimc2  25794  ellimc3  25796  limcflf  25798  cnplimc  25804  cnlimc  25805  dvreslem  25826  dvcnp2  25837  dvmulbr  25857  dvcobr  25865  cmvth  25911  dvfsumle  25942  ply1remlem  26086  fta1glem2  26090  ofmulrt  26205  plyremlem  26228  ulm2  26310  mcubic  26773  cubic2  26774  dvdsflsumcom  27114  fsumvma  27140  fsumvma2  27141  vmasum  27143  logfaclbnd  27149  dchrelbas2  27164  dchrelbas3  27165  dchrelbas4  27170  lgsquadlem1  27307  lgsquadlem2  27308  2lgslem1a  27318  eqscut2  27735  colopp  28732  colhp  28733  umgr2v2enb1  29490  upgriswlk  29604  wspthsnwspthsnon  29879  elwwlks2on  29922  elwwlks2  29929  elwspths2spth  29930  isclwwlknx  29998  clwwlkn1  30003  clwwlkn2  30006  eupth2lems  30200  fusgr2wsp2nb  30296  numclwwlkqhash  30337  isblo2  30745  ubthlem1  30832  h2hlm  30942  pjpreeq  31360  elnlfn  31890  rmounid  32457  nfpconfp  32589  fmptcof2  32614  funcnvmpt  32624  fdifsupp  32641  suppiniseg  32642  ressupprn  32646  fpwrelmapffslem  32688  nndiffz1  32742  cntzun  33034  cntrval2  33126  urpropd  33182  lindfpropd  33329  quslsm  33352  opprqus0g  33437  ressply1mon1p  33513  ply1degltel  33536  ply1degleel  33537  algextdeglem6  33688  smatrcl  33762  zarcls  33840  rhmpreimacnlem  33850  ismntop  33992  itgeq12dv  34293  eulerpartlemgvv  34343  orvcgteel  34435  reprinrn  34585  reprdifc  34594  dfrdg2  35768  broutsideof3  36099  isfne4b  36314  filnetlem4  36354  bj-elid6  37143  bj-imdirval3  37157  nlpineqsn  37381  uncf  37578  poimirlem23  37622  poimirlem26  37625  poimirlem27  37626  heicant  37634  cnambfre  37647  itg2gt0cn  37654  ftc1anclem5  37676  areacirclem5  37691  isdrngo3  37938  isidlc  37994  erimeq2  38655  prter3  38860  islshpsm  38958  islshpat  38995  lkrsc  39075  lfl1dim  39099  ldual1dim  39144  isat3  39285  glbconxN  39357  islln2  39490  islpln2  39515  islvol2  39559  cdlemg2cex  40570  diaglbN  41034  diblsmopel  41150  dihopelvalcpre  41227  xihopellsmN  41233  dihopellsm  41234  dihglbcpreN  41279  mapdval4N  41611  hdmapoc  41910  eluzp1  42280  fsuppind  42563  fsuppssindlem2  42565  prjspreln0  42582  ellz1  42740  rmydioph  42987  rmxdioph  42989  expdiophlem1  42994  expdioph  42996  pw2f1ocnv  43010  dnwech  43021  ordeldif  43231  ordeldifsucon  43232  ordeldif1o  43233  cantnfresb  43297  tfsconcat0i  43318  tfsconcatrev  43321  oadif1lem  43352  oadif1  43353  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  rfovcnvf1od  43977  k0004lem3  44122  pm14.123b  44399  rfcnpre1  44997  rfcnpre2  45009  rfcnpre3  45011  rfcnpre4  45012  climreeq  45595  funbrafv2b  47144  dfafn5a  47145  isuspgrim0  47879  gricushgr  47902  isubgrgrim  47914  rngcsectALTV  48260  ringcsectALTV  48294  elbigo2  48538  itsclc0b  48758  itscnhlinecirc02p  48771  pm5.32dav  48779  reuxfr1dd  48792  opndisj  48888  clddisj  48889  lubeldm2d  48943  glbeldm2d  48944  sectpropdlem  49022  uppropd  49167  initopropd  49229  termopropd  49230