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  3164  rexbida  3258  cbvrexdva2OLD  3334  rmobidva  3379  reubidva  3380  rmobida  3390  reubida  3391  rabbidva  3427  rabbida  3447  reuxfr1d  3740  eqrrabd  4068  mpteq12da  5209  mpteq12f  5212  mpteq12dva  5213  reuhypd  5401  xpdifid  6170  funbrfv2b  6947  dffn5  6948  feqmptdf  6960  eqfnfv2  7033  fmptco  7130  dff13  7258  riotabidva  7390  mpoeq123dva  7490  mpoeq3dva  7493  opiota  8067  fnwelem  8139  suppssr  8203  mpoxopovel  8228  mpocurryd  8277  oeeui  8623  omabs  8672  eldifsucnn  8685  qliftfun  8825  erovlem  8836  mapsnend  9059  xpcomco  9085  pw2f1olem  9099  elfi2  9437  cardval2  10014  dfac2b  10154  cflim3  10285  iundom2g  10563  fpwwe2lem7  10660  fpwwe2lem11  10664  ltexpi  10925  ordpipq  10965  axrrecex  11186  nnunb  12506  zrevaddcl  12646  qrevaddcl  12996  icoshft  13496  fznn  13615  preduz  13673  predfz  13676  fznnfl  13885  fz1isolem  14483  pfxeq  14717  pfxsuffeqwrdeq  14719  pfxsuff1eqwrdeq  14720  2swrd2eqwrdeq  14975  eqwrds3  14983  2shfti  15102  limsupgle  15496  ello12  15535  elo12  15546  isercoll  15687  sumeq2ii  15712  fsum2dlem  15789  prodeq2ii  15930  bitsmod  16456  bitscmp  16458  pwsle  17513  imasleval  17562  acsfiel  17673  ismon2  17754  isepi2  17761  oppcsect  17798  subsubc  17874  funcpropd  17923  fullpropd  17943  fucsect  17996  setcsect  18110  pltval3  18358  grpidpropd  18649  ismgmid  18652  gsumpropd2lem  18666  mgmhmpropd  18685  issubmgm2  18690  mhmpropd  18779  issubm2  18791  subgacs  19153  eqgid  19172  eqg0subg  19188  ghmqusker  19279  pgpfi2  19597  eqgabl  19825  iscyggen2  19872  cyggenod  19875  eldprd  19997  subgdmdprd  20027  dprd2d2  20037  rngpropd  20144  ringpropd  20258  crngunit  20351  dvdsrpropd  20389  isrnghmmul  20415  issubrg3  20573  rngcsect  20609  ringcsect  20643  drngpropd  20742  sdrgacs  20775  lsslss  20932  lsspropd  20989  lmhmpropd  21045  lbspropd  21071  znleval  21540  znunithash  21550  pjdm2  21698  islinds2  21800  aspval2  21885  bastop2  22967  elcls2  23047  neiptopreu  23106  maxlp  23120  restopn2  23150  iscnp3  23217  subbascn  23227  lmbr2  23232  kgencn  23529  kgencn2  23530  hauseqlcld  23619  txlm  23621  txkgen  23625  xkoptsub  23627  idqtop  23679  tgqtop  23685  qtopcld  23686  elmptrab  23800  flimopn  23948  fbflim  23949  fbflim2  23950  flimrest  23956  flffbas  23968  flftg  23969  cnflf  23975  cnflf2  23976  txflf  23979  isfcls  23982  fclsopn  23987  fclsbas  23994  fclsrest  23997  fcfnei  24008  cnfcf  24015  ptcmplem2  24026  tgphaus  24090  tsmssubm  24116  isucn2  24252  ismet2  24307  xblpnfps  24369  xblpnf  24370  blin  24395  blres  24405  elmopn2  24419  imasf1obl  24464  imasf1oxms  24465  prdsbl  24467  neibl  24477  metrest  24500  metcnp3  24516  metcnp  24517  metcnp2  24518  metcn  24519  txmetcnp  24523  txmetcn  24524  metuel2  24541  metucn  24547  ngppropd  24613  cnbl0  24749  cnblcld  24750  bl2ioo  24768  xrtgioo  24783  elcncf2  24871  cncfmet  24890  nmhmcn  25108  lmmbr  25247  lmmbr2  25248  iscfil2  25255  iscau2  25266  iscau3  25267  lmclim  25292  shft2rab  25498  sca2rab  25502  mbfeqalem1  25631  mbfmulc2lem  25637  mbfmax  25639  mbfposr  25642  mbfimaopnlem  25645  mbfaddlem  25650  mbfsup  25654  mbfinf  25655  i1fmullem  25684  i1fmulclem  25692  i1fres  25695  itg1climres  25704  mbfi1fseqlem4  25708  ibllem  25754  ellimc2  25867  ellimc3  25869  limcflf  25871  cnplimc  25877  cnlimc  25878  dvreslem  25899  dvcnp2  25910  dvmulbr  25930  dvcobr  25938  cmvth  25984  dvfsumle  26015  ply1remlem  26159  fta1glem2  26163  ofmulrt  26278  plyremlem  26301  ulm2  26383  mcubic  26845  cubic2  26846  dvdsflsumcom  27186  fsumvma  27212  fsumvma2  27213  vmasum  27215  logfaclbnd  27221  dchrelbas2  27236  dchrelbas3  27237  dchrelbas4  27242  lgsquadlem1  27379  lgsquadlem2  27380  2lgslem1a  27390  eqscut2  27806  colopp  28732  colhp  28733  umgr2v2enb1  29491  upgriswlk  29606  wspthsnwspthsnon  29883  elwwlks2on  29926  elwwlks2  29933  elwspths2spth  29934  isclwwlknx  30002  clwwlkn1  30007  clwwlkn2  30010  eupth2lems  30204  fusgr2wsp2nb  30300  numclwwlkqhash  30341  isblo2  30749  ubthlem1  30836  h2hlm  30946  pjpreeq  31364  elnlfn  31894  rmounid  32461  nfpconfp  32589  fmptcof2  32614  funcnvmpt  32624  fdifsupp  32641  suppiniseg  32642  ressupprn  32646  fpwrelmapffslem  32690  nndiffz1  32735  cntzun  33017  urpropd  33182  lindfpropd  33351  quslsm  33374  opprqus0g  33459  ressply1mon1p  33534  ply1degltel  33556  ply1degleel  33557  algextdeglem6  33704  smatrcl  33736  zarcls  33814  rhmpreimacnlem  33824  ismntop  33968  itgeq12dv  34269  eulerpartlemgvv  34319  orvcgteel  34411  reprinrn  34574  reprdifc  34583  dfrdg2  35737  broutsideof3  36068  isfne4b  36283  filnetlem4  36323  bj-elid6  37112  bj-imdirval3  37126  nlpineqsn  37350  uncf  37547  poimirlem23  37591  poimirlem26  37594  poimirlem27  37595  heicant  37603  cnambfre  37616  itg2gt0cn  37623  ftc1anclem5  37645  areacirclem5  37660  isdrngo3  37907  isidlc  37963  erimeq2  38620  prter3  38824  islshpsm  38922  islshpat  38959  lkrsc  39039  lfl1dim  39063  ldual1dim  39108  isat3  39249  glbconxN  39321  islln2  39454  islpln2  39479  islvol2  39523  cdlemg2cex  40534  diaglbN  40998  diblsmopel  41114  dihopelvalcpre  41191  xihopellsmN  41197  dihopellsm  41198  dihglbcpreN  41243  mapdval4N  41575  hdmapoc  41874  eluzp1  42286  fsuppind  42545  fsuppssindlem2  42547  prjspreln0  42564  ellz1  42723  rmydioph  42971  rmxdioph  42973  expdiophlem1  42978  expdioph  42980  pw2f1ocnv  42994  dnwech  43005  ordeldif  43216  ordeldifsucon  43217  ordeldif1o  43218  cantnfresb  43282  tfsconcat0i  43303  tfsconcatrev  43306  oadif1lem  43337  oadif1  43338  fzunt  43413  fzuntd  43414  fzunt1d  43415  fzuntgd  43416  rfovcnvf1od  43962  k0004lem3  44107  pm14.123b  44390  rfcnpre1  44969  rfcnpre2  44981  rfcnpre3  44983  rfcnpre4  44984  climreeq  45573  funbrafv2b  47117  dfafn5a  47118  isuspgrim0  47818  gricushgr  47832  isubgrgrim  47843  rngcsectALTV  48137  ringcsectALTV  48171  elbigo2  48419  itsclc0b  48639  itscnhlinecirc02p  48652  pm5.32dav  48660  reuxfr1dd  48672  opndisj  48748  clddisj  48749  lubeldm2d  48803  glbeldm2d  48804