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  3158  rexbida  3248  rmobidva  3363  reubidva  3364  rmobida  3373  reubida  3374  rabbidva  3405  rabbida  3425  reuxfr1d  3708  eqrrabd  4038  mpteq12da  5181  mpteq12f  5183  mpteq12dva  5184  reuhypd  5364  xpdifid  6126  funbrfv2b  6891  dffn5  6892  feqmptdf  6904  eqfnfv2  6977  fmptco  7074  dff13  7200  riotabidva  7334  mpoeq123dva  7432  mpoeq3dva  7435  opiota  8003  fnwelem  8073  suppssr  8137  mpoxopovel  8162  mpocurryd  8211  oeeui  8530  omabs  8579  eldifsucnn  8592  qliftfun  8739  erovlem  8750  mapsnend  8973  xpcomco  8995  pw2f1olem  9009  elfi2  9317  cardval2  9903  dfac2b  10041  cflim3  10172  iundom2g  10450  fpwwe2lem7  10548  fpwwe2lem11  10552  ltexpi  10813  ordpipq  10853  axrrecex  11074  nnunb  12397  zrevaddcl  12536  qrevaddcl  12884  icoshft  13389  fznn  13508  preduz  13566  predfz  13569  fznnfl  13782  fz1isolem  14384  pfxeq  14619  pfxsuffeqwrdeq  14621  pfxsuff1eqwrdeq  14622  2swrd2eqwrdeq  14876  eqwrds3  14884  2shfti  15003  limsupgle  15400  ello12  15439  elo12  15450  isercoll  15591  sumeq2ii  15616  fsum2dlem  15693  prodeq2ii  15834  bitsmod  16363  bitscmp  16365  pwsle  17413  imasleval  17462  acsfiel  17577  ismon2  17658  isepi2  17665  oppcsect  17702  subsubc  17777  funcpropd  17826  fullpropd  17846  fucsect  17899  setcsect  18013  pltval3  18260  grpidpropd  18587  ismgmid  18590  gsumpropd2lem  18604  mgmhmpropd  18623  issubmgm2  18628  mhmpropd  18717  issubm2  18729  subgacs  19090  eqgid  19109  eqg0subg  19125  ghmqusker  19216  pgpfi2  19535  eqgabl  19763  iscyggen2  19810  cyggenod  19813  eldprd  19935  subgdmdprd  19965  dprd2d2  19975  rngpropd  20109  ringpropd  20223  crngunit  20314  dvdsrpropd  20352  isrnghmmul  20378  issubrg3  20533  rngcsect  20569  ringcsect  20603  drngpropd  20702  sdrgacs  20734  lsslss  20912  lsspropd  20969  lmhmpropd  21025  lbspropd  21051  znleval  21509  znunithash  21519  pjdm2  21666  islinds2  21768  aspval2  21854  bastop2  22938  elcls2  23018  neiptopreu  23077  maxlp  23091  restopn2  23121  iscnp3  23188  subbascn  23198  lmbr2  23203  kgencn  23500  kgencn2  23501  hauseqlcld  23590  txlm  23592  txkgen  23596  xkoptsub  23598  idqtop  23650  tgqtop  23656  qtopcld  23657  elmptrab  23771  flimopn  23919  fbflim  23920  fbflim2  23921  flimrest  23927  flffbas  23939  flftg  23940  cnflf  23946  cnflf2  23947  txflf  23950  isfcls  23953  fclsopn  23958  fclsbas  23965  fclsrest  23968  fcfnei  23979  cnfcf  23986  ptcmplem2  23997  tgphaus  24061  tsmssubm  24087  isucn2  24222  ismet2  24277  xblpnfps  24339  xblpnf  24340  blin  24365  blres  24375  elmopn2  24389  imasf1obl  24432  imasf1oxms  24433  prdsbl  24435  neibl  24445  metrest  24468  metcnp3  24484  metcnp  24485  metcnp2  24486  metcn  24487  txmetcnp  24491  txmetcn  24492  metuel2  24509  metucn  24515  ngppropd  24581  cnbl0  24717  cnblcld  24718  bl2ioo  24736  xrtgioo  24751  elcncf2  24839  cncfmet  24858  nmhmcn  25076  lmmbr  25214  lmmbr2  25215  iscfil2  25222  iscau2  25233  iscau3  25234  lmclim  25259  shft2rab  25465  sca2rab  25469  mbfeqalem1  25598  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  mbfimaopnlem  25612  mbfaddlem  25617  mbfsup  25621  mbfinf  25622  i1fmullem  25651  i1fmulclem  25659  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  ibllem  25721  ellimc2  25834  ellimc3  25836  limcflf  25838  cnplimc  25844  cnlimc  25845  dvreslem  25866  dvcnp2  25877  dvmulbr  25897  dvcobr  25905  cmvth  25951  dvfsumle  25982  ply1remlem  26126  fta1glem2  26130  ofmulrt  26245  plyremlem  26268  ulm2  26350  mcubic  26813  cubic2  26814  dvdsflsumcom  27154  fsumvma  27180  fsumvma2  27181  vmasum  27183  logfaclbnd  27189  dchrelbas2  27204  dchrelbas3  27205  dchrelbas4  27210  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1a  27358  eqcuts2  27782  colopp  28841  colhp  28842  umgr2v2enb1  29600  upgriswlk  29714  wspthsnwspthsnon  29989  elwwlks2on  30034  elwwlks2  30042  elwspths2spth  30043  isclwwlknx  30111  clwwlkn1  30116  clwwlkn2  30119  eupth2lems  30313  fusgr2wsp2nb  30409  numclwwlkqhash  30450  isblo2  30858  ubthlem1  30945  h2hlm  31055  pjpreeq  31473  elnlfn  32003  rmounid  32569  nfpconfp  32710  fmptcof2  32735  funcnvmpt  32745  fdifsupp  32764  suppiniseg  32765  ressupprn  32769  fpwrelmapffslem  32811  nndiffz1  32866  cntzun  33161  cntrval2  33253  urpropd  33313  lindfpropd  33463  quslsm  33486  opprqus0g  33571  ressply1mon1p  33649  ply1degltel  33675  ply1degleel  33676  algextdeglem6  33879  smatrcl  33953  zarcls  34031  rhmpreimacnlem  34041  ismntop  34183  itgeq12dv  34483  eulerpartlemgvv  34533  orvcgteel  34625  reprinrn  34775  reprdifc  34784  dfrdg2  35987  broutsideof3  36320  isfne4b  36535  filnetlem4  36575  bj-elid6  37371  bj-imdirval3  37385  nlpineqsn  37609  uncf  37796  poimirlem23  37840  poimirlem26  37843  poimirlem27  37844  heicant  37852  cnambfre  37865  itg2gt0cn  37872  ftc1anclem5  37894  areacirclem5  37909  isdrngo3  38156  isidlc  38212  erimeq2  38933  prter3  39138  islshpsm  39236  islshpat  39273  lkrsc  39353  lfl1dim  39377  ldual1dim  39422  isat3  39563  glbconxN  39634  islln2  39767  islpln2  39792  islvol2  39836  cdlemg2cex  40847  diaglbN  41311  diblsmopel  41427  dihopelvalcpre  41504  xihopellsmN  41510  dihopellsm  41511  dihglbcpreN  41556  mapdval4N  41888  hdmapoc  42187  eluzp1  42558  fsuppind  42829  fsuppssindlem2  42831  prjspreln0  42848  ellz1  43005  rmydioph  43252  rmxdioph  43254  expdiophlem1  43259  expdioph  43261  pw2f1ocnv  43275  dnwech  43286  ordeldif  43496  ordeldifsucon  43497  ordeldif1o  43498  cantnfresb  43562  tfsconcat0i  43583  tfsconcatrev  43586  oadif1lem  43617  oadif1  43618  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  rfovcnvf1od  44241  k0004lem3  44386  pm14.123b  44663  rfcnpre1  45260  rfcnpre2  45272  rfcnpre3  45274  rfcnpre4  45275  climreeq  45855  funbrafv2b  47401  dfafn5a  47402  isuspgrim0  48136  gricushgr  48159  isubgrgrim  48171  rngcsectALTV  48517  ringcsectALTV  48551  elbigo2  48794  itsclc0b  49014  itscnhlinecirc02p  49027  pm5.32dav  49035  reuxfr1dd  49048  opndisj  49144  clddisj  49145  lubeldm2d  49199  glbeldm2d  49200  sectpropdlem  49277  uppropd  49422  initopropd  49484  termopropd  49485