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  3185  rexbida  3275  rmobidva  3379  reubidva  3380  rmobida  3389  reubida  3390  rabbidva  3419  rabbida  3438  reuxfr1d  3708  eqrrabd  4034  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  reuhypd  5381  xpdifid  6158  xpdifcnvepel  6159  funbrfv2b  6934  dffn5  6935  feqmptdf  6947  funcnvmpt  6987  eqfnfv2  7022  fmptco  7122  dff13  7250  riotabidva  7388  mpoeq123dva  7486  mpoeq3dva  7489  opiota  8059  fnwelem  8132  suppssr  8196  mpoxopovel  8221  mpocurryd  8270  oeeui  8595  omabs  8644  eldifsucnn  8657  qliftfun  8807  erovlem  8818  uncf  8875  mapsnend  9048  xpcomco  9070  pw2f1olem  9084  elfi2  9390  cardval2  10053  dfac2b  10190  cflim3  10321  iundom2g  10605  fpwwe2lem7  10703  fpwwe2lem11  10707  ltexpi  10968  ordpipq  11008  axrrecex  11229  nnunb  12583  zrevaddcl  12722  qrevaddcl  13080  icoshft  13585  fznn  13706  preduz  13764  predfz  13767  fznnfl  13982  fz1isolem  14586  pfxeq  14825  pfxsuffeqwrdeq  14827  pfxsuff1eqwrdeq  14828  2swrd2eqwrdeq  15086  eqwrds3  15094  2shfti  15213  limsupgle  15624  ello12  15663  elo12  15674  isercoll  15815  sumeq2ii  15840  fsum2dlem  15916  prodeq2ii  16060  bitsmod  16586  bitscmp  16588  pwsle  17644  imasleval  17693  acsfiel  17808  ismon2  17889  isepi2  17896  oppcsect  17933  subsubc  18008  funcpropd  18057  fullpropd  18077  fucsect  18130  setcsect  18244  pltval3  18491  grpidpropd  18822  ismgmid  18825  gsumpropd2lem  18848  mgmhmpropd  18867  issubmgm2  18872  mhmpropd  18967  issubm2  18979  subgacs  19351  eqgid  19372  eqg0subg  19391  ghmqusker  19481  pgpfi2  19800  eqgabl  20028  iscyggen2  20075  cyggenod  20078  eldprd  20200  subgdmdprd  20230  dprd2d2  20240  rngpropd  20376  ringpropd  20499  crngunit  20588  dvdsrpropd  20626  isrnghmmul  20652  issubrg3  20832  rngcsect  20868  ringcsect  20902  drngpropd  21007  sdrgacs  21038  lsslss  21216  lsspropd  21272  lmhmpropd  21328  lbspropd  21354  df2idl2crng  21557  znleval  21840  znunithash  21850  pjdm2  21997  islinds2  22099  aspval2  22186  bastop2  23292  elcls2  23372  neiptopreu  23431  maxlp  23445  restopn2  23475  iscnp3  23542  subbascn  23552  lmbr2  23557  kgencn  23855  kgencn2  23856  hauseqlcld  23945  txlm  23947  txkgen  23951  xkoptsub  23953  idqtop  24005  tgqtop  24011  qtopcld  24012  elmptrab  24126  flimopn  24274  fbflim  24275  fbflim2  24276  flimrest  24282  flffbas  24294  flftg  24295  cnflf  24301  cnflf2  24302  txflf  24305  isfcls  24308  fclsopn  24313  fclsbas  24320  fclsrest  24323  fcfnei  24334  cnfcf  24341  ptcmplem2  24352  tgphaus  24416  tsmssubm  24442  isucn2  24577  ismet2  24632  xblpnfps  24694  xblpnf  24695  blin  24720  blres  24730  elmopn2  24744  imasf1obl  24787  imasf1oxms  24788  prdsbl  24790  neibl  24800  metrest  24823  metcnp3  24839  metcnp  24840  metcnp2  24841  metcn  24842  txmetcnp  24846  txmetcn  24847  metuel2  24864  metucn  24870  ngppropd  24936  cnbl0  25072  cnblcld  25073  bl2ioo  25091  xrtgioo  25106  elcncf2  25191  cncfmet  25210  nmhmcn  25421  lmmbr  25559  lmmbr2  25560  iscfil2  25567  iscau2  25578  iscau3  25579  lmclim  25604  shft2rab  25809  sca2rab  25813  mbfeqalem1  25942  mbfmulc2lem  25948  mbfmax  25950  mbfposr  25953  mbfimaopnlem  25956  mbfaddlem  25961  mbfsup  25965  mbfinf  25966  i1fmullem  25995  i1fmulclem  26003  i1fres  26006  itg1climres  26015  mbfi1fseqlem4  26019  ibllem  26065  ellimc2  26177  ellimc3  26179  limcflf  26181  cnplimc  26187  cnlimc  26188  dvreslem  26209  dvcnp2  26220  dvmulbr  26239  dvcobr  26246  cmvth  26291  dvfsumle  26321  ply1remlem  26463  fta1glem2  26467  ofmulrt  26582  plyremlem  26607  rnplynfin  26612  ulm2  26694  mcubic  27157  cubic2  27158  dvdsflsumcom  27497  fsumvma  27522  fsumvma2  27523  vmasum  27525  logfaclbnd  27531  dchrelbas2  27546  dchrelbas3  27547  dchrelbas4  27552  lgsquadlem1  27689  lgsquadlem2  27690  2lgslem1a  27700  eqcuts2  28154  colopp  29229  colhp  29230  angmgmaddcpbl  29372  dfprlng2  29407  umgr2v2enb1  30089  upgriswlk  30203  wspthsnwspthsnon  30487  elwwlks2on  30532  elwwlks2  30540  elwspths2spth  30541  isclwwlknx  30609  clwwlkn1  30614  clwwlkn2  30617  eupth2lems  30821  fusgr2wsp2nb  30917  numclwwlkqhash  30958  isblo2  31367  ubthlem1  31454  h2hlm  31564  pjpreeq  31982  elnlfn  32512  rmounid  33073  nfpconfp  33208  fmptcof2  33233  fdifsupp  33260  suppiniseg  33261  ressupprn  33265  fpwrelmapffslem  33306  nndiffz1  33360  cntzun  33622  cntrval2  33714  urpropd  33773  lindfpropd  33919  quslsm  33938  opprqus0g  33996  ressply1mon1p  34082  ply1degltel  34108  ply1degleel  34109  algextdeglem6  34336  smatrcl  34410  zarcls  34488  rhmpreimacnlem  34498  ismntop  34640  itgeq12dv  34941  eulerpartlemgvv  34991  orvcgteel  35083  reprinrn  35230  reprdifc  35239  dfrdg2  36527  broutsideof3  36861  isfne4b  37099  filnetlem4  37139  bj-elid6  38059  bj-imdirval3  38073  nlpineqsn  38299  poimirlem23  38529  poimirlem26  38532  poimirlem27  38533  heicant  38541  cnambfre  38554  itg2gt0cn  38561  ftc1anclem5  38583  areacirclem5  38598  isdrngo3  38861  isidlc  38917  erimeq2  39663  prter3  39907  islshpsm  40005  islshpat  40042  lkrsc  40122  lfl1dim  40146  ldual1dim  40191  isat3  40332  glbconxN  40403  islln2  40536  islpln2  40561  islvol2  40605  cdlemg2cex  41616  diaglbN  42080  diblsmopel  42196  dihopelvalcpre  42273  xihopellsmN  42279  dihopellsm  42280  dihglbcpreN  42325  mapdval4N  42657  hdmapoc  42956  eluzp1  43332  fsuppind  43580  fsuppssindlem2  43582  prjspreln0  43599  ellz1  43731  rmydioph  43974  rmxdioph  43976  expdiophlem1  43981  expdioph  43983  pw2f1ocnv  43997  dnwech  44008  ordeldif  44218  ordeldifsucon  44219  ordeldif1o  44220  cantnfresb  44284  tfsconcat0i  44305  tfsconcatrev  44308  oadif1lem  44339  oadif1  44340  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  rfovcnvf1od  44963  k0004lem3  45108  pm14.123b  45369  rfcnpre1  45979  rfcnpre2  45991  rfcnpre3  45993  rfcnpre4  45994  climreeq  46569  funbrafv2b  48173  dfafn5a  48174  isuspgrim0  48936  gricushgr  48959  isubgrgrim  48971  rngcsectALTV  49316  ringcsectALTV  49350  elbigo2  49608  itsclc0b  49828  itscnhlinecirc02p  49841  pm5.32rda  49848  reuxfr1dd  49861  opndisj  49955  clddisj  49956  lubeldm2d  50010  glbeldm2d  50011  sectpropdlem  50088  uppropd  50233  initopropd  50295  termopropd  50296