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  3160  rexbida  3250  rmobidva  3356  reubidva  3357  rmobida  3366  reubida  3367  rabbidva  3396  rabbida  3416  reuxfr1d  3697  eqrrabd  4027  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  reuhypd  5356  xpdifid  6126  funbrfv2b  6891  dffn5  6892  feqmptdf  6904  funcnvmpt  6943  eqfnfv2  6978  fmptco  7076  dff13  7202  riotabidva  7336  mpoeq123dva  7434  mpoeq3dva  7437  opiota  8005  fnwelem  8074  suppssr  8138  mpoxopovel  8163  mpocurryd  8212  oeeui  8531  omabs  8580  eldifsucnn  8593  qliftfun  8742  erovlem  8753  mapsnend  8976  xpcomco  8998  pw2f1olem  9012  elfi2  9320  cardval2  9906  dfac2b  10044  cflim3  10175  iundom2g  10453  fpwwe2lem7  10551  fpwwe2lem11  10555  ltexpi  10816  ordpipq  10856  axrrecex  11077  nnunb  12424  zrevaddcl  12563  qrevaddcl  12912  icoshft  13417  fznn  13537  preduz  13595  predfz  13598  fznnfl  13812  fz1isolem  14414  pfxeq  14649  pfxsuffeqwrdeq  14651  pfxsuff1eqwrdeq  14652  2swrd2eqwrdeq  14906  eqwrds3  14914  2shfti  15033  limsupgle  15430  ello12  15469  elo12  15480  isercoll  15621  sumeq2ii  15646  fsum2dlem  15723  prodeq2ii  15867  bitsmod  16396  bitscmp  16398  pwsle  17447  imasleval  17496  acsfiel  17611  ismon2  17692  isepi2  17699  oppcsect  17736  subsubc  17811  funcpropd  17860  fullpropd  17880  fucsect  17933  setcsect  18047  pltval3  18294  grpidpropd  18621  ismgmid  18624  gsumpropd2lem  18638  mgmhmpropd  18657  issubmgm2  18662  mhmpropd  18751  issubm2  18763  subgacs  19127  eqgid  19146  eqg0subg  19162  ghmqusker  19253  pgpfi2  19572  eqgabl  19800  iscyggen2  19847  cyggenod  19850  eldprd  19972  subgdmdprd  20002  dprd2d2  20012  rngpropd  20146  ringpropd  20260  crngunit  20349  dvdsrpropd  20387  isrnghmmul  20413  issubrg3  20568  rngcsect  20604  ringcsect  20638  drngpropd  20737  sdrgacs  20769  lsslss  20947  lsspropd  21004  lmhmpropd  21060  lbspropd  21086  znleval  21544  znunithash  21554  pjdm2  21701  islinds2  21803  aspval2  21888  bastop2  22969  elcls2  23049  neiptopreu  23108  maxlp  23122  restopn2  23152  iscnp3  23219  subbascn  23229  lmbr2  23234  kgencn  23531  kgencn2  23532  hauseqlcld  23621  txlm  23623  txkgen  23627  xkoptsub  23629  idqtop  23681  tgqtop  23687  qtopcld  23688  elmptrab  23802  flimopn  23950  fbflim  23951  fbflim2  23952  flimrest  23958  flffbas  23970  flftg  23971  cnflf  23977  cnflf2  23978  txflf  23981  isfcls  23984  fclsopn  23989  fclsbas  23996  fclsrest  23999  fcfnei  24010  cnfcf  24017  ptcmplem2  24028  tgphaus  24092  tsmssubm  24118  isucn2  24253  ismet2  24308  xblpnfps  24370  xblpnf  24371  blin  24396  blres  24406  elmopn2  24420  imasf1obl  24463  imasf1oxms  24464  prdsbl  24466  neibl  24476  metrest  24499  metcnp3  24515  metcnp  24516  metcnp2  24517  metcn  24518  txmetcnp  24522  txmetcn  24523  metuel2  24540  metucn  24546  ngppropd  24612  cnbl0  24748  cnblcld  24749  bl2ioo  24767  xrtgioo  24782  elcncf2  24867  cncfmet  24886  nmhmcn  25097  lmmbr  25235  lmmbr2  25236  iscfil2  25243  iscau2  25254  iscau3  25255  lmclim  25280  shft2rab  25485  sca2rab  25489  mbfeqalem1  25618  mbfmulc2lem  25624  mbfmax  25626  mbfposr  25629  mbfimaopnlem  25632  mbfaddlem  25637  mbfsup  25641  mbfinf  25642  i1fmullem  25671  i1fmulclem  25679  i1fres  25682  itg1climres  25691  mbfi1fseqlem4  25695  ibllem  25741  ellimc2  25854  ellimc3  25856  limcflf  25858  cnplimc  25864  cnlimc  25865  dvreslem  25886  dvcnp2  25897  dvmulbr  25916  dvcobr  25923  cmvth  25968  dvfsumle  25998  ply1remlem  26140  fta1glem2  26144  ofmulrt  26258  plyremlem  26281  ulm2  26363  mcubic  26824  cubic2  26825  dvdsflsumcom  27165  fsumvma  27190  fsumvma2  27191  vmasum  27193  logfaclbnd  27199  dchrelbas2  27214  dchrelbas3  27215  dchrelbas4  27220  lgsquadlem1  27357  lgsquadlem2  27358  2lgslem1a  27368  eqcuts2  27792  colopp  28851  colhp  28852  umgr2v2enb1  29610  upgriswlk  29724  wspthsnwspthsnon  29999  elwwlks2on  30044  elwwlks2  30052  elwspths2spth  30053  isclwwlknx  30121  clwwlkn1  30126  clwwlkn2  30129  eupth2lems  30323  fusgr2wsp2nb  30419  numclwwlkqhash  30460  isblo2  30869  ubthlem1  30956  h2hlm  31066  pjpreeq  31484  elnlfn  32014  rmounid  32579  nfpconfp  32720  fmptcof2  32745  fdifsupp  32773  suppiniseg  32774  ressupprn  32778  fpwrelmapffslem  32820  nndiffz1  32874  cntzun  33155  cntrval2  33247  urpropd  33307  lindfpropd  33457  quslsm  33480  opprqus0g  33565  ressply1mon1p  33643  ply1degltel  33669  ply1degleel  33670  algextdeglem6  33882  smatrcl  33956  zarcls  34034  rhmpreimacnlem  34044  ismntop  34186  itgeq12dv  34486  eulerpartlemgvv  34536  orvcgteel  34628  reprinrn  34778  reprdifc  34787  dfrdg2  35991  broutsideof3  36324  isfne4b  36539  filnetlem4  36579  bj-elid6  37500  bj-imdirval3  37514  nlpineqsn  37738  uncf  37934  poimirlem23  37978  poimirlem26  37981  poimirlem27  37982  heicant  37990  cnambfre  38003  itg2gt0cn  38010  ftc1anclem5  38032  areacirclem5  38047  isdrngo3  38294  isidlc  38350  erimeq2  39098  prter3  39342  islshpsm  39440  islshpat  39477  lkrsc  39557  lfl1dim  39581  ldual1dim  39626  isat3  39767  glbconxN  39838  islln2  39971  islpln2  39996  islvol2  40040  cdlemg2cex  41051  diaglbN  41515  diblsmopel  41631  dihopelvalcpre  41708  xihopellsmN  41714  dihopellsm  41715  dihglbcpreN  41760  mapdval4N  42092  hdmapoc  42391  eluzp1  42753  fsuppind  43037  fsuppssindlem2  43039  prjspreln0  43056  ellz1  43213  rmydioph  43460  rmxdioph  43462  expdiophlem1  43467  expdioph  43469  pw2f1ocnv  43483  dnwech  43494  ordeldif  43704  ordeldifsucon  43705  ordeldif1o  43706  cantnfresb  43770  tfsconcat0i  43791  tfsconcatrev  43794  oadif1lem  43825  oadif1  43826  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  rfovcnvf1od  44449  k0004lem3  44594  pm14.123b  44871  rfcnpre1  45468  rfcnpre2  45480  rfcnpre3  45482  rfcnpre4  45483  climreeq  46061  funbrafv2b  47619  dfafn5a  47620  isuspgrim0  48382  gricushgr  48405  isubgrgrim  48417  rngcsectALTV  48763  ringcsectALTV  48797  elbigo2  49040  itsclc0b  49260  itscnhlinecirc02p  49273  pm5.32dav  49281  reuxfr1dd  49294  opndisj  49390  clddisj  49391  lubeldm2d  49445  glbeldm2d  49446  sectpropdlem  49523  uppropd  49668  initopropd  49730  termopropd  49731