Theorem pm5.32da 580

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  rexbidva  3177  rexbida  3270  cbvrexdva2OLD  3347  rmobidva  3392  reubidva  3393  rmobida  3403  reubida  3404  rabbidva  3440  rabbida  3459  reuxfr1d  3747  mpteq12da  5234  mpteq12f  5237  mpteq12dva  5238  reuhypd  5418  xpdifid  6168  funbrfv2b  6950  dffn5  6951  feqmptdf  6963  eqfnfv2  7034  fmptco  7127  dff13  7254  riotabidva  7385  mpoeq123dva  7483  mpoeq3dva  7486  opiota  8045  fnwelem  8117  suppssr  8181  mpoxopovel  8205  mpocurryd  8254  oeeui  8602  omabs  8650  eldifsucnn  8663  qliftfun  8796  erovlem  8807  mapsnend  9036  xpcomco  9062  pw2f1olem  9076  elfi2  9409  cardval2  9986  dfac2b  10125  cflim3  10257  iundom2g  10535  fpwwe2lem7  10632  fpwwe2lem11  10636  ltexpi  10897  ordpipq  10937  axrrecex  11158  nnunb  12468  zrevaddcl  12607  qrevaddcl  12955  icoshft  13450  fznn  13569  preduz  13623  predfz  13626  fznnfl  13827  fz1isolem  14422  pfxeq  14646  pfxsuffeqwrdeq  14648  pfxsuff1eqwrdeq  14649  2swrd2eqwrdeq  14904  eqwrds3  14912  2shfti  15027  limsupgle  15421  ello12  15460  elo12  15471  isercoll  15614  sumeq2ii  15639  fsum2dlem  15716  prodeq2ii  15857  bitsmod  16377  bitscmp  16379  pwsle  17438  imasleval  17487  acsfiel  17598  ismon2  17681  isepi2  17688  oppcsect  17725  subsubc  17803  funcpropd  17851  fullpropd  17871  fucsect  17925  setcsect  18039  pltval3  18292  grpidpropd  18581  ismgmid  18584  gsumpropd2lem  18598  mhmpropd  18678  issubm2  18685  subgacs  19041  eqgid  19060  eqg0subg  19073  pgpfi2  19474  eqgabl  19702  iscyggen2  19749  cyggenod  19752  eldprd  19874  subgdmdprd  19904  dprd2d2  19914  ringpropd  20102  crngunit  20192  dvdsrpropd  20230  issubrg3  20347  drngpropd  20394  sdrgacs  20417  lsslss  20572  lsspropd  20628  lmhmpropd  20684  lbspropd  20710  znleval  21110  znunithash  21120  pjdm2  21266  islinds2  21368  aspval2  21452  bastop2  22497  elcls2  22578  neiptopreu  22637  maxlp  22651  restopn2  22681  iscnp3  22748  subbascn  22758  lmbr2  22763  kgencn  23060  kgencn2  23061  hauseqlcld  23150  txlm  23152  txkgen  23156  xkoptsub  23158  idqtop  23210  tgqtop  23216  qtopcld  23217  elmptrab  23331  flimopn  23479  fbflim  23480  fbflim2  23481  flimrest  23487  flffbas  23499  flftg  23500  cnflf  23506  cnflf2  23507  txflf  23510  isfcls  23513  fclsopn  23518  fclsbas  23525  fclsrest  23528  fcfnei  23539  cnfcf  23546  ptcmplem2  23557  tgphaus  23621  tsmssubm  23647  isucn2  23784  ismet2  23839  xblpnfps  23901  xblpnf  23902  blin  23927  blres  23937  elmopn2  23951  imasf1obl  23997  imasf1oxms  23998  prdsbl  24000  neibl  24010  metrest  24033  metcnp3  24049  metcnp  24050  metcnp2  24051  metcn  24052  txmetcnp  24056  txmetcn  24057  metuel2  24074  metucn  24080  ngppropd  24146  cnbl0  24290  cnblcld  24291  bl2ioo  24308  xrtgioo  24322  elcncf2  24406  cncfmet  24425  nmhmcn  24636  lmmbr  24775  lmmbr2  24776  iscfil2  24783  iscau2  24794  iscau3  24795  lmclim  24820  shft2rab  25025  sca2rab  25029  mbfeqalem1  25158  mbfmulc2lem  25164  mbfmax  25166  mbfposr  25169  mbfimaopnlem  25172  mbfaddlem  25177  mbfsup  25181  mbfinf  25182  i1fmullem  25211  i1fmulclem  25220  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  ibllem  25282  ellimc2  25394  ellimc3  25396  limcflf  25398  cnplimc  25404  cnlimc  25405  dvreslem  25426  ply1remlem  25680  fta1glem2  25684  ofmulrt  25795  plyremlem  25817  ulm2  25897  mcubic  26352  cubic2  26353  dvdsflsumcom  26692  fsumvma  26716  fsumvma2  26717  vmasum  26719  logfaclbnd  26725  dchrelbas2  26740  dchrelbas3  26741  dchrelbas4  26746  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1a  26894  eqscut2  27307  colopp  28020  colhp  28021  umgr2v2enb1  28783  upgriswlk  28898  wspthsnwspthsnon  29170  elwwlks2on  29213  elwwlks2  29220  elwspths2spth  29221  isclwwlknx  29289  clwwlkn1  29294  clwwlkn2  29297  eupth2lems  29491  fusgr2wsp2nb  29587  numclwwlkqhash  29628  isblo2  30036  ubthlem1  30123  h2hlm  30233  pjpreeq  30651  elnlfn  31181  rmounid  31735  eqrrabd  31741  nfpconfp  31856  fmptcof2  31882  funcnvmpt  31892  suppiniseg  31908  ressupprn  31912  fpwrelmapffslem  31957  nndiffz1  31997  cntzun  32212  urpropd  32378  lindfpropd  32498  quslsm  32516  ghmqusker  32532  opprqus0g  32604  ressply1mon1p  32657  ply1degltel  32666  smatrcl  32776  zarcls  32854  rhmpreimacnlem  32864  ismntop  33006  itgeq12dv  33325  eulerpartlemgvv  33375  orvcgteel  33466  reprinrn  33630  reprdifc  33639  dfrdg2  34767  broutsideof3  35098  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  gg-cmvth  35181  gg-dvfsumle  35182  isfne4b  35226  filnetlem4  35266  bj-elid6  36051  bj-imdirval3  36065  nlpineqsn  36289  uncf  36467  poimirlem23  36511  poimirlem26  36514  poimirlem27  36515  heicant  36523  cnambfre  36536  itg2gt0cn  36543  ftc1anclem5  36565  areacirclem5  36580  isdrngo3  36827  isidlc  36883  erimeq2  37548  prter3  37752  islshpsm  37850  islshpat  37887  lkrsc  37967  lfl1dim  37991  ldual1dim  38036  isat3  38177  glbconxN  38249  islln2  38382  islpln2  38407  islvol2  38451  cdlemg2cex  39462  diaglbN  39926  diblsmopel  40042  dihopelvalcpre  40119  xihopellsmN  40125  dihopellsm  40126  dihglbcpreN  40171  mapdval4N  40503  hdmapoc  40802  fsuppind  41162  fsuppssindlem2  41164  prjspreln0  41351  ellz1  41505  rmydioph  41753  rmxdioph  41755  expdiophlem1  41760  expdioph  41762  pw2f1ocnv  41776  dnwech  41790  ordeldif  42008  ordeldifsucon  42009  ordeldif1o  42010  cantnfresb  42074  tfsconcat0i  42095  tfsconcatrev  42098  oadif1lem  42129  oadif1  42130  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  rfovcnvf1od  42755  k0004lem3  42900  pm14.123b  43185  rfcnpre1  43703  rfcnpre2  43715  rfcnpre3  43717  rfcnpre4  43718  climreeq  44329  funbrafv2b  45867  dfafn5a  45868  isomushgr  46494  isomuspgr  46502  mgmhmpropd  46555  issubmgm2  46560  rngpropd  46673  isrnghmmul  46691  rngcsect  46878  rngcsectALTV  46890  ringcsect  46929  ringcsectALTV  46953  elbigo2  47238  itsclc0b  47458  itscnhlinecirc02p  47471  pm5.32dav  47479  opndisj  47535  clddisj  47536  lubeldm2d  47591  glbeldm2d  47592