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  3163  rexbida  3258  cbvrexdva2OLD  3333  rmobidva  3379  reubidva  3380  rmobida  3390  reubida  3391  rabbidva  3427  rabbida  3447  reuxfr1d  3738  eqrrabd  4066  mpteq12da  5208  mpteq12f  5210  mpteq12dva  5211  reuhypd  5394  xpdifid  6162  funbrfv2b  6941  dffn5  6942  feqmptdf  6954  eqfnfv2  7027  fmptco  7124  dff13  7252  riotabidva  7386  mpoeq123dva  7486  mpoeq3dva  7489  opiota  8063  fnwelem  8135  suppssr  8199  mpoxopovel  8224  mpocurryd  8273  oeeui  8619  omabs  8668  eldifsucnn  8681  qliftfun  8821  erovlem  8832  mapsnend  9055  xpcomco  9081  pw2f1olem  9095  elfi2  9431  cardval2  10010  dfac2b  10150  cflim3  10281  iundom2g  10559  fpwwe2lem7  10656  fpwwe2lem11  10660  ltexpi  10921  ordpipq  10961  axrrecex  11182  nnunb  12502  zrevaddcl  12642  qrevaddcl  12992  icoshft  13495  fznn  13614  preduz  13672  predfz  13675  fznnfl  13884  fz1isolem  14484  pfxeq  14719  pfxsuffeqwrdeq  14721  pfxsuff1eqwrdeq  14722  2swrd2eqwrdeq  14977  eqwrds3  14985  2shfti  15104  limsupgle  15498  ello12  15537  elo12  15548  isercoll  15689  sumeq2ii  15714  fsum2dlem  15791  prodeq2ii  15932  bitsmod  16460  bitscmp  16462  pwsle  17511  imasleval  17560  acsfiel  17671  ismon2  17752  isepi2  17759  oppcsect  17796  subsubc  17871  funcpropd  17920  fullpropd  17940  fucsect  17993  setcsect  18107  pltval3  18354  grpidpropd  18645  ismgmid  18648  gsumpropd2lem  18662  mgmhmpropd  18681  issubmgm2  18686  mhmpropd  18775  issubm2  18787  subgacs  19149  eqgid  19168  eqg0subg  19184  ghmqusker  19275  pgpfi2  19592  eqgabl  19820  iscyggen2  19867  cyggenod  19870  eldprd  19992  subgdmdprd  20022  dprd2d2  20032  rngpropd  20139  ringpropd  20253  crngunit  20343  dvdsrpropd  20381  isrnghmmul  20407  issubrg3  20565  rngcsect  20601  ringcsect  20635  drngpropd  20734  sdrgacs  20766  lsslss  20923  lsspropd  20980  lmhmpropd  21036  lbspropd  21062  znleval  21520  znunithash  21530  pjdm2  21676  islinds2  21778  aspval2  21863  bastop2  22937  elcls2  23017  neiptopreu  23076  maxlp  23090  restopn2  23120  iscnp3  23187  subbascn  23197  lmbr2  23202  kgencn  23499  kgencn2  23500  hauseqlcld  23589  txlm  23591  txkgen  23595  xkoptsub  23597  idqtop  23649  tgqtop  23655  qtopcld  23656  elmptrab  23770  flimopn  23918  fbflim  23919  fbflim2  23920  flimrest  23926  flffbas  23938  flftg  23939  cnflf  23945  cnflf2  23946  txflf  23949  isfcls  23952  fclsopn  23957  fclsbas  23964  fclsrest  23967  fcfnei  23978  cnfcf  23985  ptcmplem2  23996  tgphaus  24060  tsmssubm  24086  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  25215  lmmbr2  25216  iscfil2  25223  iscau2  25234  iscau3  25235  lmclim  25260  shft2rab  25466  sca2rab  25470  mbfeqalem1  25599  mbfmulc2lem  25605  mbfmax  25607  mbfposr  25610  mbfimaopnlem  25613  mbfaddlem  25618  mbfsup  25622  mbfinf  25623  i1fmullem  25652  i1fmulclem  25660  i1fres  25663  itg1climres  25672  mbfi1fseqlem4  25676  ibllem  25722  ellimc2  25835  ellimc3  25837  limcflf  25839  cnplimc  25845  cnlimc  25846  dvreslem  25867  dvcnp2  25878  dvmulbr  25898  dvcobr  25906  cmvth  25952  dvfsumle  25983  ply1remlem  26127  fta1glem2  26131  ofmulrt  26246  plyremlem  26269  ulm2  26351  mcubic  26814  cubic2  26815  dvdsflsumcom  27155  fsumvma  27181  fsumvma2  27182  vmasum  27184  logfaclbnd  27190  dchrelbas2  27205  dchrelbas3  27206  dchrelbas4  27211  lgsquadlem1  27348  lgsquadlem2  27349  2lgslem1a  27359  eqscut2  27775  colopp  28753  colhp  28754  umgr2v2enb1  29511  upgriswlk  29626  wspthsnwspthsnon  29903  elwwlks2on  29946  elwwlks2  29953  elwspths2spth  29954  isclwwlknx  30022  clwwlkn1  30027  clwwlkn2  30030  eupth2lems  30224  fusgr2wsp2nb  30320  numclwwlkqhash  30361  isblo2  30769  ubthlem1  30856  h2hlm  30966  pjpreeq  31384  elnlfn  31914  rmounid  32481  nfpconfp  32615  fmptcof2  32640  funcnvmpt  32650  fdifsupp  32667  suppiniseg  32668  ressupprn  32672  fpwrelmapffslem  32714  nndiffz1  32768  cntzun  33067  urpropd  33232  lindfpropd  33402  quslsm  33425  opprqus0g  33510  ressply1mon1p  33586  ply1degltel  33609  ply1degleel  33610  algextdeglem6  33761  smatrcl  33832  zarcls  33910  rhmpreimacnlem  33920  ismntop  34062  itgeq12dv  34363  eulerpartlemgvv  34413  orvcgteel  34505  reprinrn  34655  reprdifc  34664  dfrdg2  35818  broutsideof3  36149  isfne4b  36364  filnetlem4  36404  bj-elid6  37193  bj-imdirval3  37207  nlpineqsn  37431  uncf  37628  poimirlem23  37672  poimirlem26  37675  poimirlem27  37676  heicant  37684  cnambfre  37697  itg2gt0cn  37704  ftc1anclem5  37726  areacirclem5  37741  isdrngo3  37988  isidlc  38044  erimeq2  38701  prter3  38905  islshpsm  39003  islshpat  39040  lkrsc  39120  lfl1dim  39144  ldual1dim  39189  isat3  39330  glbconxN  39402  islln2  39535  islpln2  39560  islvol2  39604  cdlemg2cex  40615  diaglbN  41079  diblsmopel  41195  dihopelvalcpre  41272  xihopellsmN  41278  dihopellsm  41279  dihglbcpreN  41324  mapdval4N  41656  hdmapoc  41955  eluzp1  42325  fsuppind  42588  fsuppssindlem2  42590  prjspreln0  42607  ellz1  42765  rmydioph  43013  rmxdioph  43015  expdiophlem1  43020  expdioph  43022  pw2f1ocnv  43036  dnwech  43047  ordeldif  43257  ordeldifsucon  43258  ordeldif1o  43259  cantnfresb  43323  tfsconcat0i  43344  tfsconcatrev  43347  oadif1lem  43378  oadif1  43379  fzunt  43454  fzuntd  43455  fzunt1d  43456  fzuntgd  43457  rfovcnvf1od  44003  k0004lem3  44148  pm14.123b  44425  rfcnpre1  45023  rfcnpre2  45035  rfcnpre3  45037  rfcnpre4  45038  climreeq  45622  funbrafv2b  47168  dfafn5a  47169  isuspgrim0  47887  gricushgr  47910  isubgrgrim  47922  rngcsectALTV  48230  ringcsectALTV  48264  elbigo2  48512  itsclc0b  48732  itscnhlinecirc02p  48745  pm5.32dav  48753  reuxfr1dd  48765  opndisj  48857  clddisj  48858  lubeldm2d  48912  glbeldm2d  48913  sectpropdlem  48983  initopropd  49140  termopropd  49141