Theorem pm5.32da 584

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  bian1d  585  rexbidva  3162  rexbida  3252  rmobidva  3358  reubidva  3359  rmobida  3368  reubida  3369  rabbidva  3398  rabbida  3418  reuxfr1d  3698  eqrrabd  4024  mpteq12da  5162  mpteq12f  5164  mpteq12dva  5165  reuhypd  5355  xpdifid  6126  funbrfv2b  6891  dffn5  6892  feqmptdf  6904  funcnvmpt  6944  eqfnfv2  6979  fmptco  7078  dff13  7205  riotabidva  7339  mpoeq123dva  7437  mpoeq3dva  7440  opiota  8008  fnwelem  8078  suppssr  8142  mpoxopovel  8167  mpocurryd  8216  oeeui  8535  omabs  8584  eldifsucnn  8597  qliftfun  8746  erovlem  8757  mapsnend  8980  xpcomco  9002  pw2f1olem  9016  elfi2  9324  cardval2  9913  dfac2b  10051  cflim3  10182  iundom2g  10460  fpwwe2lem7  10558  fpwwe2lem11  10562  ltexpi  10823  ordpipq  10863  axrrecex  11084  nnunb  12431  zrevaddcl  12570  qrevaddcl  12919  icoshft  13424  fznn  13544  preduz  13602  predfz  13605  fznnfl  13819  fz1isolem  14421  pfxeq  14656  pfxsuffeqwrdeq  14658  pfxsuff1eqwrdeq  14659  2swrd2eqwrdeq  14913  eqwrds3  14921  2shfti  15040  limsupgle  15437  ello12  15476  elo12  15487  isercoll  15628  sumeq2ii  15653  fsum2dlem  15730  prodeq2ii  15874  bitsmod  16403  bitscmp  16405  pwsle  17454  imasleval  17503  acsfiel  17618  ismon2  17699  isepi2  17706  oppcsect  17743  subsubc  17818  funcpropd  17867  fullpropd  17887  fucsect  17940  setcsect  18054  pltval3  18301  grpidpropd  18628  ismgmid  18631  gsumpropd2lem  18645  mgmhmpropd  18664  issubmgm2  18669  mhmpropd  18758  issubm2  18770  subgacs  19134  eqgid  19153  eqg0subg  19169  ghmqusker  19260  pgpfi2  19579  eqgabl  19807  iscyggen2  19854  cyggenod  19857  eldprd  19979  subgdmdprd  20009  dprd2d2  20019  rngpropd  20153  ringpropd  20267  crngunit  20356  dvdsrpropd  20394  isrnghmmul  20420  issubrg3  20579  rngcsect  20615  ringcsect  20649  drngpropd  20748  sdrgacs  20780  lsslss  20958  lsspropd  21014  lmhmpropd  21070  lbspropd  21096  znleval  21536  znunithash  21546  pjdm2  21693  islinds2  21795  aspval2  21880  bastop2  22984  elcls2  23064  neiptopreu  23123  maxlp  23137  restopn2  23167  iscnp3  23234  subbascn  23244  lmbr2  23249  kgencn  23546  kgencn2  23547  hauseqlcld  23636  txlm  23638  txkgen  23642  xkoptsub  23644  idqtop  23696  tgqtop  23702  qtopcld  23703  elmptrab  23817  flimopn  23965  fbflim  23966  fbflim2  23967  flimrest  23973  flffbas  23985  flftg  23986  cnflf  23992  cnflf2  23993  txflf  23996  isfcls  23999  fclsopn  24004  fclsbas  24011  fclsrest  24014  fcfnei  24025  cnfcf  24032  ptcmplem2  24043  tgphaus  24107  tsmssubm  24133  isucn2  24268  ismet2  24323  xblpnfps  24385  xblpnf  24386  blin  24411  blres  24421  elmopn2  24435  imasf1obl  24478  imasf1oxms  24479  prdsbl  24481  neibl  24491  metrest  24514  metcnp3  24530  metcnp  24531  metcnp2  24532  metcn  24533  txmetcnp  24537  txmetcn  24538  metuel2  24555  metucn  24561  ngppropd  24627  cnbl0  24763  cnblcld  24764  bl2ioo  24782  xrtgioo  24797  elcncf2  24882  cncfmet  24901  nmhmcn  25112  lmmbr  25250  lmmbr2  25251  iscfil2  25258  iscau2  25269  iscau3  25270  lmclim  25295  shft2rab  25500  sca2rab  25504  mbfeqalem1  25633  mbfmulc2lem  25639  mbfmax  25641  mbfposr  25644  mbfimaopnlem  25647  mbfaddlem  25652  mbfsup  25656  mbfinf  25657  i1fmullem  25686  i1fmulclem  25694  i1fres  25697  itg1climres  25706  mbfi1fseqlem4  25710  ibllem  25756  ellimc2  25869  ellimc3  25871  limcflf  25873  cnplimc  25879  cnlimc  25880  dvreslem  25901  dvcnp2  25912  dvmulbr  25931  dvcobr  25938  cmvth  25983  dvfsumle  26013  ply1remlem  26155  fta1glem2  26159  ofmulrt  26273  plyremlem  26295  ulm2  26375  mcubic  26836  cubic2  26837  dvdsflsumcom  27176  fsumvma  27201  fsumvma2  27202  vmasum  27204  logfaclbnd  27210  dchrelbas2  27225  dchrelbas3  27226  dchrelbas4  27231  lgsquadlem1  27368  lgsquadlem2  27369  2lgslem1a  27379  eqcuts2  27803  colopp  28862  colhp  28863  umgr2v2enb1  29620  upgriswlk  29734  wspthsnwspthsnon  30009  elwwlks2on  30054  elwwlks2  30062  elwspths2spth  30063  isclwwlknx  30131  clwwlkn1  30136  clwwlkn2  30139  eupth2lems  30333  fusgr2wsp2nb  30429  numclwwlkqhash  30470  isblo2  30879  ubthlem1  30966  h2hlm  31076  pjpreeq  31494  elnlfn  32024  rmounid  32589  nfpconfp  32731  fmptcof2  32756  fdifsupp  32784  suppiniseg  32785  ressupprn  32789  fpwrelmapffslem  32831  nndiffz1  32885  cntzun  33167  cntrval2  33259  urpropd  33319  lindfpropd  33472  quslsm  33495  opprqus0g  33580  ressply1mon1p  33658  ply1degltel  33684  ply1degleel  33685  algextdeglem6  33913  smatrcl  33987  zarcls  34065  rhmpreimacnlem  34075  ismntop  34217  itgeq12dv  34517  eulerpartlemgvv  34567  orvcgteel  34659  reprinrn  34809  reprdifc  34818  dfrdg2  36028  broutsideof3  36361  isfne4b  36576  filnetlem4  36616  bj-elid6  37537  bj-imdirval3  37551  nlpineqsn  37777  uncf  37973  poimirlem23  38017  poimirlem26  38020  poimirlem27  38021  heicant  38029  cnambfre  38042  itg2gt0cn  38049  ftc1anclem5  38071  areacirclem5  38086  isdrngo3  38333  isidlc  38389  erimeq2  39137  prter3  39381  islshpsm  39479  islshpat  39516  lkrsc  39596  lfl1dim  39620  ldual1dim  39665  isat3  39806  glbconxN  39877  islln2  40010  islpln2  40035  islvol2  40079  cdlemg2cex  41090  diaglbN  41554  diblsmopel  41670  dihopelvalcpre  41747  xihopellsmN  41753  dihopellsm  41754  dihglbcpreN  41799  mapdval4N  42131  hdmapoc  42430  eluzp1  42791  fsuppind  43047  fsuppssindlem2  43049  prjspreln0  43066  ellz1  43223  rmydioph  43466  rmxdioph  43468  expdiophlem1  43473  expdioph  43475  pw2f1ocnv  43489  dnwech  43500  ordeldif  43710  ordeldifsucon  43711  ordeldif1o  43712  cantnfresb  43776  tfsconcat0i  43797  tfsconcatrev  43800  oadif1lem  43831  oadif1  43832  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  rfovcnvf1od  44455  k0004lem3  44600  pm14.123b  44877  rfcnpre1  45474  rfcnpre2  45486  rfcnpre3  45488  rfcnpre4  45489  climreeq  46065  funbrafv2b  47629  dfafn5a  47630  isuspgrim0  48392  gricushgr  48415  isubgrgrim  48427  rngcsectALTV  48773  ringcsectALTV  48807  elbigo2  49050  itsclc0b  49270  itscnhlinecirc02p  49283  pm5.32dav  49291  reuxfr1dd  49304  opndisj  49400  clddisj  49401  lubeldm2d  49455  glbeldm2d  49456  sectpropdlem  49533  uppropd  49678  initopropd  49740  termopropd  49741