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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  rexbidva  3226  rexbida  3252  reubida  3322  reubidva  3323  rmobida  3327  rmobidva  3328  cbvrexdva2  3394  rabbidva  3414  reuxfr1d  3686  mpteq12da  5160  mpteq12f  5163  mpteq12dva  5164  reuhypd  5343  xpdifid  6076  funbrfv2b  6836  dffn5  6837  feqmptdf  6848  eqfnfv2  6919  fmptco  7010  dff13  7137  riotabidva  7261  mpoeq123dva  7358  mpoeq3dva  7361  opiota  7908  fnwelem  7981  suppssr  8021  mpoxopovel  8045  mpocurryd  8094  oeeui  8442  omabs  8490  eldifsucnn  8503  qliftfun  8600  erovlem  8611  mapsnend  8835  xpcomco  8858  pw2f1olem  8872  elfi2  9182  cardval2  9758  dfac2b  9895  cflim3  10027  iundom2g  10305  fpwwe2lem7  10402  fpwwe2lem11  10406  ltexpi  10667  ordpipq  10707  axrrecex  10928  nnunb  12238  zrevaddcl  12374  qrevaddcl  12720  icoshft  13214  fznn  13333  preduz  13387  predfz  13390  fznnfl  13591  fz1isolem  14184  pfxeq  14418  pfxsuffeqwrdeq  14420  pfxsuff1eqwrdeq  14421  2swrd2eqwrdeq  14675  eqwrds3  14685  2shfti  14800  limsupgle  15195  ello12  15234  elo12  15245  isercoll  15388  sumeq2ii  15414  fsum2dlem  15491  prodeq2ii  15632  bitsmod  16152  bitscmp  16154  pwsle  17212  imasleval  17261  acsfiel  17372  ismon2  17455  isepi2  17462  oppcsect  17499  subsubc  17577  funcpropd  17625  fullpropd  17645  fucsect  17699  setcsect  17813  pltval3  18066  grpidpropd  18355  ismgmid  18358  gsumpropd2lem  18372  mhmpropd  18445  issubm2  18452  subgacs  18798  eqgid  18817  pgpfi2  19220  eqgabl  19445  iscyggen2  19490  cyggenod  19493  eldprd  19616  subgdmdprd  19646  dprd2d2  19656  ringpropd  19830  crngunit  19913  dvdsrpropd  19947  drngpropd  20027  issubrg3  20061  sdrgacs  20078  lsslss  20232  lsspropd  20288  lmhmpropd  20344  lbspropd  20370  znleval  20771  znunithash  20781  pjdm2  20927  islinds2  21029  aspval2  21111  bastop2  22153  elcls2  22234  neiptopreu  22293  maxlp  22307  restopn2  22337  iscnp3  22404  subbascn  22414  lmbr2  22419  kgencn  22716  kgencn2  22717  hauseqlcld  22806  txlm  22808  txkgen  22812  xkoptsub  22814  idqtop  22866  tgqtop  22872  qtopcld  22873  elmptrab  22987  flimopn  23135  fbflim  23136  fbflim2  23137  flimrest  23143  flffbas  23155  flftg  23156  cnflf  23162  cnflf2  23163  txflf  23166  isfcls  23169  fclsopn  23174  fclsbas  23181  fclsrest  23184  fcfnei  23195  cnfcf  23202  ptcmplem2  23213  tgphaus  23277  tsmssubm  23303  isucn2  23440  ismet2  23495  xblpnfps  23557  xblpnf  23558  blin  23583  blres  23593  elmopn2  23607  imasf1obl  23653  imasf1oxms  23654  prdsbl  23656  neibl  23666  metrest  23689  metcnp3  23705  metcnp  23706  metcnp2  23707  metcn  23708  txmetcnp  23712  txmetcn  23713  metuel2  23730  metucn  23736  ngppropd  23802  cnbl0  23946  cnblcld  23947  bl2ioo  23964  xrtgioo  23978  elcncf2  24062  cncfmet  24081  nmhmcn  24292  lmmbr  24431  lmmbr2  24432  iscfil2  24439  iscau2  24450  iscau3  24451  lmclim  24476  shft2rab  24681  sca2rab  24685  mbfeqalem1  24814  mbfmulc2lem  24820  mbfmax  24822  mbfposr  24825  mbfimaopnlem  24828  mbfaddlem  24833  mbfsup  24837  mbfinf  24838  i1fmullem  24867  i1fmulclem  24876  i1fres  24879  itg1climres  24888  mbfi1fseqlem4  24892  ibllem  24938  ellimc2  25050  ellimc3  25052  limcflf  25054  cnplimc  25060  cnlimc  25061  dvreslem  25082  ply1remlem  25336  fta1glem2  25340  ofmulrt  25451  plyremlem  25473  ulm2  25553  mcubic  26006  cubic2  26007  dvdsflsumcom  26346  fsumvma  26370  fsumvma2  26371  vmasum  26373  logfaclbnd  26379  dchrelbas2  26394  dchrelbas3  26395  dchrelbas4  26400  lgsquadlem1  26537  lgsquadlem2  26538  2lgslem1a  26548  colopp  27139  colhp  27140  umgr2v2enb1  27902  upgriswlk  28017  wspthsnwspthsnon  28290  elwwlks2on  28333  elwwlks2  28340  elwspths2spth  28341  isclwwlknx  28409  clwwlkn1  28414  clwwlkn2  28417  eupth2lems  28611  fusgr2wsp2nb  28707  numclwwlkqhash  28748  isblo2  29154  ubthlem1  29241  h2hlm  29351  pjpreeq  29769  elnlfn  30299  rmounid  30852  eqrrabd  30858  nfpconfp  30976  fmptcof2  31003  funcnvmpt  31013  suppiniseg  31029  ressupprn  31033  fpwrelmapffslem  31076  nndiffz1  31116  cntzun  31329  lindfpropd  31585  quslsm  31602  smatrcl  31755  zarcls  31833  rhmpreimacnlem  31843  ismntop  31985  itgeq12dv  32302  eulerpartlemgvv  32352  orvcgteel  32443  reprinrn  32607  reprdifc  32616  dfrdg2  33780  eqscut2  34009  broutsideof3  34437  isfne4b  34539  filnetlem4  34579  bj-elid6  35350  bj-imdirval3  35364  nlpineqsn  35588  uncf  35765  poimirlem23  35809  poimirlem26  35812  poimirlem27  35813  heicant  35821  cnambfre  35834  itg2gt0cn  35841  ftc1anclem5  35863  areacirclem5  35878  isdrngo3  36126  isidlc  36182  erim2  36796  prter3  36903  islshpsm  37001  islshpat  37038  lkrsc  37118  lfl1dim  37142  ldual1dim  37187  isat3  37328  glbconxN  37399  islln2  37532  islpln2  37557  islvol2  37601  cdlemg2cex  38612  diaglbN  39076  diblsmopel  39192  dihopelvalcpre  39269  xihopellsmN  39275  dihopellsm  39276  dihglbcpreN  39321  mapdval4N  39653  hdmapoc  39952  fsuppind  40286  fsuppssindlem2  40288  prjspreln0  40455  ellz1  40596  rmydioph  40843  rmxdioph  40845  expdiophlem1  40850  expdioph  40852  pw2f1ocnv  40866  dnwech  40880  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  rfovcnvf1od  41619  k0004lem3  41766  pm14.123b  42051  rfcnpre1  42569  rfcnpre2  42581  rfcnpre3  42583  rfcnpre4  42584  climreeq  43161  funbrafv2b  44662  dfafn5a  44663  isomushgr  45289  isomuspgr  45297  mgmhmpropd  45350  issubmgm2  45355  isrnghmmul  45462  rngcsect  45549  rngcsectALTV  45561  ringcsect  45600  ringcsectALTV  45624  elbigo2  45909  itsclc0b  46129  itscnhlinecirc02p  46142  pm5.32dav  46150  opndisj  46207  clddisj  46208  lubeldm2d  46263  glbeldm2d  46264