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  34748  eulerpartlemgvv  34798  orvcgteel  34890  reprinrn  35037  reprdifc  35046  dfrdg2  36306  broutsideof3  36639  isfne4b  36893  filnetlem4  36933  bj-elid6  37855  bj-imdirval3  37869  nlpineqsn  38095  uncf  38291  poimirlem23  38335  poimirlem26  38338  poimirlem27  38339  heicant  38347  cnambfre  38360  itg2gt0cn  38367  ftc1anclem5  38389  areacirclem5  38404  isdrngo3  38651  isidlc  38707  erimeq2  39453  prter3  39697  islshpsm  39795  islshpat  39832  lkrsc  39912  lfl1dim  39936  ldual1dim  39981  isat3  40122  glbconxN  40193  islln2  40326  islpln2  40351  islvol2  40395  cdlemg2cex  41406  diaglbN  41870  diblsmopel  41986  dihopelvalcpre  42063  xihopellsmN  42069  dihopellsm  42070  dihglbcpreN  42115  mapdval4N  42447  hdmapoc  42746  eluzp1  43109  fsuppind  43363  fsuppssindlem2  43365  prjspreln0  43382  ellz1  43539  rmydioph  43782  rmxdioph  43784  expdiophlem1  43789  expdioph  43791  pw2f1ocnv  43805  dnwech  43816  ordeldif  44026  ordeldifsucon  44027  ordeldif1o  44028  cantnfresb  44092  tfsconcat0i  44113  tfsconcatrev  44116  oadif1lem  44147  oadif1  44148  fzunt  44222  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  rfovcnvf1od  44771  k0004lem3  44916  pm14.123b  45177  rfcnpre1  45780  rfcnpre2  45792  rfcnpre3  45794  rfcnpre4  45795  climreeq  46370  funbrafv2b  47937  dfafn5a  47938  isuspgrim0  48700  gricushgr  48723  isubgrgrim  48735  rngcsectALTV  49081  ringcsectALTV  49115  elbigo2  49373  itsclc0b  49593  itscnhlinecirc02p  49606  pm5.32dav  49613  reuxfr1dd  49626  opndisj  49722  clddisj  49723  lubeldm2d  49777  glbeldm2d  49778  sectpropdlem  49855  uppropd  50000  initopropd  50062  termopropd  50063