Theorem pm5.32da 590

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bian1d  591  rexbidva  3190  rexbida  3280  rmobidva  3385  reubidva  3386  rmobida  3395  reubida  3396  rabbidva  3425  rabbida  3445  reuxfr1d  3716  eqrrabd  4043  mpteq12da  5199  mpteq12f  5201  mpteq12dva  5202  reuhypd  5395  xpdifid  6170  xpdifcnvepel  6171  funbrfv2b  6945  dffn5  6946  feqmptdf  6958  funcnvmpt  6998  eqfnfv2  7033  fmptco  7132  dff13  7259  riotabidva  7399  mpoeq123dva  7497  mpoeq3dva  7500  opiota  8065  fnwelem  8136  suppssr  8200  mpoxopovel  8225  mpocurryd  8274  oeeui  8597  omabs  8646  eldifsucnn  8659  qliftfun  8809  erovlem  8820  mapsnend  9043  xpcomco  9065  pw2f1olem  9079  elfi2  9384  cardval2  9996  dfac2b  10133  cflim3  10264  iundom2g  10542  fpwwe2lem7  10640  fpwwe2lem11  10644  ltexpi  10905  ordpipq  10945  axrrecex  11166  nnunb  12518  zrevaddcl  12657  qrevaddcl  13013  icoshft  13518  fznn  13639  preduz  13697  predfz  13700  fznnfl  13915  fz1isolem  14518  pfxeq  14757  pfxsuffeqwrdeq  14759  pfxsuff1eqwrdeq  14760  2swrd2eqwrdeq  15016  eqwrds3  15024  2shfti  15143  limsupgle  15554  ello12  15593  elo12  15604  isercoll  15745  sumeq2ii  15770  fsum2dlem  15847  prodeq2ii  15991  bitsmod  16519  bitscmp  16521  pwsle  17571  imasleval  17620  acsfiel  17735  ismon2  17816  isepi2  17823  oppcsect  17860  subsubc  17935  funcpropd  17984  fullpropd  18004  fucsect  18057  setcsect  18171  pltval3  18418  grpidpropd  18745  ismgmid  18748  gsumpropd2lem  18766  mgmhmpropd  18785  issubmgm2  18790  mhmpropd  18881  issubm2  18893  subgacs  19258  eqgid  19279  eqg0subg  19298  ghmqusker  19388  pgpfi2  19707  eqgabl  19935  iscyggen2  19982  cyggenod  19985  eldprd  20107  subgdmdprd  20137  dprd2d2  20147  rngpropd  20283  ringpropd  20404  crngunit  20493  dvdsrpropd  20531  isrnghmmul  20557  issubrg3  20736  rngcsect  20772  ringcsect  20806  drngpropd  20910  sdrgacs  20941  lsslss  21119  lsspropd  21175  lmhmpropd  21231  lbspropd  21257  df2idl2crng  21458  znleval  21741  znunithash  21751  pjdm2  21898  islinds2  22000  aspval2  22085  bastop2  23188  elcls2  23268  neiptopreu  23327  maxlp  23341  restopn2  23371  iscnp3  23438  subbascn  23448  lmbr2  23453  kgencn  23750  kgencn2  23751  hauseqlcld  23840  txlm  23842  txkgen  23846  xkoptsub  23848  idqtop  23900  tgqtop  23906  qtopcld  23907  elmptrab  24021  flimopn  24169  fbflim  24170  fbflim2  24171  flimrest  24177  flffbas  24189  flftg  24190  cnflf  24196  cnflf2  24197  txflf  24200  isfcls  24203  fclsopn  24208  fclsbas  24215  fclsrest  24218  fcfnei  24229  cnfcf  24236  ptcmplem2  24247  tgphaus  24311  tsmssubm  24337  isucn2  24472  ismet2  24527  xblpnfps  24589  xblpnf  24590  blin  24615  blres  24625  elmopn2  24639  imasf1obl  24682  imasf1oxms  24683  prdsbl  24685  neibl  24695  metrest  24718  metcnp3  24734  metcnp  24735  metcnp2  24736  metcn  24737  txmetcnp  24741  txmetcn  24742  metuel2  24759  metucn  24765  ngppropd  24831  cnbl0  24967  cnblcld  24968  bl2ioo  24986  xrtgioo  25001  elcncf2  25086  cncfmet  25105  nmhmcn  25316  lmmbr  25454  lmmbr2  25455  iscfil2  25462  iscau2  25473  iscau3  25474  lmclim  25499  shft2rab  25704  sca2rab  25708  mbfeqalem1  25837  mbfmulc2lem  25843  mbfmax  25845  mbfposr  25848  mbfimaopnlem  25851  mbfaddlem  25856  mbfsup  25860  mbfinf  25861  i1fmullem  25890  i1fmulclem  25898  i1fres  25901  itg1climres  25910  mbfi1fseqlem4  25914  ibllem  25960  ellimc2  26073  ellimc3  26075  limcflf  26077  cnplimc  26083  cnlimc  26084  dvreslem  26105  dvcnp2  26116  dvmulbr  26135  dvcobr  26142  cmvth  26187  dvfsumle  26217  ply1remlem  26359  fta1glem2  26363  ofmulrt  26477  plyremlem  26502  ulm2  26585  mcubic  27049  cubic2  27050  dvdsflsumcom  27389  fsumvma  27414  fsumvma2  27415  vmasum  27417  logfaclbnd  27423  dchrelbas2  27438  dchrelbas3  27439  dchrelbas4  27444  lgsquadlem1  27581  lgsquadlem2  27582  2lgslem1a  27592  eqcuts2  28016  colopp  29088  colhp  29089  dfprlng2  29234  umgr2v2enb1  29913  upgriswlk  30027  wspthsnwspthsnon  30302  elwwlks2on  30347  elwwlks2  30355  elwspths2spth  30356  isclwwlknx  30424  clwwlkn1  30429  clwwlkn2  30432  eupth2lems  30626  fusgr2wsp2nb  30722  numclwwlkqhash  30763  isblo2  31172  ubthlem1  31259  h2hlm  31369  pjpreeq  31787  elnlfn  32317  rmounid  32878  nfpconfp  33014  fmptcof2  33039  fdifsupp  33067  suppiniseg  33068  ressupprn  33072  fpwrelmapffslem  33114  nndiffz1  33168  cntzun  33430  cntrval2  33522  urpropd  33581  lindfpropd  33726  quslsm  33745  opprqus0g  33803  ressply1mon1p  33889  ply1degltel  33915  ply1degleel  33916  algextdeglem6  34143  smatrcl  34217  zarcls  34295  rhmpreimacnlem  34305  ismntop  34447  itgeq12dv  34747  eulerpartlemgvv  34797  orvcgteel  34889  reprinrn  35036  reprdifc  35045  dfrdg2  36305  broutsideof3  36638  isfne4b  36892  filnetlem4  36932  bj-elid6  37854  bj-imdirval3  37868  nlpineqsn  38094  uncf  38290  poimirlem23  38334  poimirlem26  38337  poimirlem27  38338  heicant  38346  cnambfre  38359  itg2gt0cn  38366  ftc1anclem5  38388  areacirclem5  38403  isdrngo3  38650  isidlc  38706  erimeq2  39452  prter3  39696  islshpsm  39794  islshpat  39831  lkrsc  39911  lfl1dim  39935  ldual1dim  39980  isat3  40121  glbconxN  40192  islln2  40325  islpln2  40350  islvol2  40394  cdlemg2cex  41405  diaglbN  41869  diblsmopel  41985  dihopelvalcpre  42062  xihopellsmN  42068  dihopellsm  42069  dihglbcpreN  42114  mapdval4N  42446  hdmapoc  42745  eluzp1  43108  fsuppind  43362  fsuppssindlem2  43364  prjspreln0  43381  ellz1  43538  rmydioph  43781  rmxdioph  43783  expdiophlem1  43788  expdioph  43790  pw2f1ocnv  43804  dnwech  43815  ordeldif  44025  ordeldifsucon  44026  ordeldif1o  44027  cantnfresb  44091  tfsconcat0i  44112  tfsconcatrev  44115  oadif1lem  44146  oadif1  44147  fzunt  44221  fzuntd  44222  fzunt1d  44223  fzuntgd  44224  rfovcnvf1od  44770  k0004lem3  44915  pm14.123b  45176  rfcnpre1  45779  rfcnpre2  45791  rfcnpre3  45793  rfcnpre4  45794  climreeq  46369  funbrafv2b  47936  dfafn5a  47937  isuspgrim0  48699  gricushgr  48722  isubgrgrim  48734  rngcsectALTV  49080  ringcsectALTV  49114  elbigo2  49372  itsclc0b  49592  itscnhlinecirc02p  49605  pm5.32dav  49612  reuxfr1dd  49625  opndisj  49721  clddisj  49722  lubeldm2d  49776  glbeldm2d  49777  sectpropdlem  49854  uppropd  49999  initopropd  50061  termopropd  50062