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:  bian1d  580  rexbidva  3160  rexbida  3250  rmobidva  3365  reubidva  3366  rmobida  3375  reubida  3376  rabbidva  3407  rabbida  3427  reuxfr1d  3710  eqrrabd  4040  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  reuhypd  5366  xpdifid  6134  funbrfv2b  6899  dffn5  6900  feqmptdf  6912  funcnvmpt  6951  eqfnfv2  6986  fmptco  7084  dff13  7210  riotabidva  7344  mpoeq123dva  7442  mpoeq3dva  7445  opiota  8013  fnwelem  8083  suppssr  8147  mpoxopovel  8172  mpocurryd  8221  oeeui  8540  omabs  8589  eldifsucnn  8602  qliftfun  8751  erovlem  8762  mapsnend  8985  xpcomco  9007  pw2f1olem  9021  elfi2  9329  cardval2  9915  dfac2b  10053  cflim3  10184  iundom2g  10462  fpwwe2lem7  10560  fpwwe2lem11  10564  ltexpi  10825  ordpipq  10865  axrrecex  11086  nnunb  12409  zrevaddcl  12548  qrevaddcl  12896  icoshft  13401  fznn  13520  preduz  13578  predfz  13581  fznnfl  13794  fz1isolem  14396  pfxeq  14631  pfxsuffeqwrdeq  14633  pfxsuff1eqwrdeq  14634  2swrd2eqwrdeq  14888  eqwrds3  14896  2shfti  15015  limsupgle  15412  ello12  15451  elo12  15462  isercoll  15603  sumeq2ii  15628  fsum2dlem  15705  prodeq2ii  15846  bitsmod  16375  bitscmp  16377  pwsle  17425  imasleval  17474  acsfiel  17589  ismon2  17670  isepi2  17677  oppcsect  17714  subsubc  17789  funcpropd  17838  fullpropd  17858  fucsect  17911  setcsect  18025  pltval3  18272  grpidpropd  18599  ismgmid  18602  gsumpropd2lem  18616  mgmhmpropd  18635  issubmgm2  18640  mhmpropd  18729  issubm2  18741  subgacs  19102  eqgid  19121  eqg0subg  19137  ghmqusker  19228  pgpfi2  19547  eqgabl  19775  iscyggen2  19822  cyggenod  19825  eldprd  19947  subgdmdprd  19977  dprd2d2  19987  rngpropd  20121  ringpropd  20235  crngunit  20326  dvdsrpropd  20364  isrnghmmul  20390  issubrg3  20545  rngcsect  20581  ringcsect  20615  drngpropd  20714  sdrgacs  20746  lsslss  20924  lsspropd  20981  lmhmpropd  21037  lbspropd  21063  znleval  21521  znunithash  21531  pjdm2  21678  islinds2  21780  aspval2  21866  bastop2  22950  elcls2  23030  neiptopreu  23089  maxlp  23103  restopn2  23133  iscnp3  23200  subbascn  23210  lmbr2  23215  kgencn  23512  kgencn2  23513  hauseqlcld  23602  txlm  23604  txkgen  23608  xkoptsub  23610  idqtop  23662  tgqtop  23668  qtopcld  23669  elmptrab  23783  flimopn  23931  fbflim  23932  fbflim2  23933  flimrest  23939  flffbas  23951  flftg  23952  cnflf  23958  cnflf2  23959  txflf  23962  isfcls  23965  fclsopn  23970  fclsbas  23977  fclsrest  23980  fcfnei  23991  cnfcf  23998  ptcmplem2  24009  tgphaus  24073  tsmssubm  24099  isucn2  24234  ismet2  24289  xblpnfps  24351  xblpnf  24352  blin  24377  blres  24387  elmopn2  24401  imasf1obl  24444  imasf1oxms  24445  prdsbl  24447  neibl  24457  metrest  24480  metcnp3  24496  metcnp  24497  metcnp2  24498  metcn  24499  txmetcnp  24503  txmetcn  24504  metuel2  24521  metucn  24527  ngppropd  24593  cnbl0  24729  cnblcld  24730  bl2ioo  24748  xrtgioo  24763  elcncf2  24851  cncfmet  24870  nmhmcn  25088  lmmbr  25226  lmmbr2  25227  iscfil2  25234  iscau2  25245  iscau3  25246  lmclim  25271  shft2rab  25477  sca2rab  25481  mbfeqalem1  25610  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  mbfimaopnlem  25624  mbfaddlem  25629  mbfsup  25633  mbfinf  25634  i1fmullem  25663  i1fmulclem  25671  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  ibllem  25733  ellimc2  25846  ellimc3  25848  limcflf  25850  cnplimc  25856  cnlimc  25857  dvreslem  25878  dvcnp2  25889  dvmulbr  25909  dvcobr  25917  cmvth  25963  dvfsumle  25994  ply1remlem  26138  fta1glem2  26142  ofmulrt  26257  plyremlem  26280  ulm2  26362  mcubic  26825  cubic2  26826  dvdsflsumcom  27166  fsumvma  27192  fsumvma2  27193  vmasum  27195  logfaclbnd  27201  dchrelbas2  27216  dchrelbas3  27217  dchrelbas4  27222  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1a  27370  eqcuts2  27794  colopp  28853  colhp  28854  umgr2v2enb1  29612  upgriswlk  29726  wspthsnwspthsnon  30001  elwwlks2on  30046  elwwlks2  30054  elwspths2spth  30055  isclwwlknx  30123  clwwlkn1  30128  clwwlkn2  30131  eupth2lems  30325  fusgr2wsp2nb  30421  numclwwlkqhash  30462  isblo2  30870  ubthlem1  30957  h2hlm  31067  pjpreeq  31485  elnlfn  32015  rmounid  32580  nfpconfp  32721  fmptcof2  32746  fdifsupp  32774  suppiniseg  32775  ressupprn  32779  fpwrelmapffslem  32821  nndiffz1  32876  cntzun  33172  cntrval2  33264  urpropd  33324  lindfpropd  33474  quslsm  33497  opprqus0g  33582  ressply1mon1p  33660  ply1degltel  33686  ply1degleel  33687  algextdeglem6  33899  smatrcl  33973  zarcls  34051  rhmpreimacnlem  34061  ismntop  34203  itgeq12dv  34503  eulerpartlemgvv  34553  orvcgteel  34645  reprinrn  34795  reprdifc  34804  dfrdg2  36006  broutsideof3  36339  isfne4b  36554  filnetlem4  36594  bj-elid6  37419  bj-imdirval3  37433  nlpineqsn  37657  uncf  37844  poimirlem23  37888  poimirlem26  37891  poimirlem27  37892  heicant  37900  cnambfre  37913  itg2gt0cn  37920  ftc1anclem5  37942  areacirclem5  37957  isdrngo3  38204  isidlc  38260  erimeq2  39008  prter3  39252  islshpsm  39350  islshpat  39387  lkrsc  39467  lfl1dim  39491  ldual1dim  39536  isat3  39677  glbconxN  39748  islln2  39881  islpln2  39906  islvol2  39950  cdlemg2cex  40961  diaglbN  41425  diblsmopel  41541  dihopelvalcpre  41618  xihopellsmN  41624  dihopellsm  41625  dihglbcpreN  41670  mapdval4N  42002  hdmapoc  42301  eluzp1  42671  fsuppind  42942  fsuppssindlem2  42944  prjspreln0  42961  ellz1  43118  rmydioph  43365  rmxdioph  43367  expdiophlem1  43372  expdioph  43374  pw2f1ocnv  43388  dnwech  43399  ordeldif  43609  ordeldifsucon  43610  ordeldif1o  43611  cantnfresb  43675  tfsconcat0i  43696  tfsconcatrev  43699  oadif1lem  43730  oadif1  43731  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  rfovcnvf1od  44354  k0004lem3  44499  pm14.123b  44776  rfcnpre1  45373  rfcnpre2  45385  rfcnpre3  45387  rfcnpre4  45388  climreeq  45967  funbrafv2b  47513  dfafn5a  47514  isuspgrim0  48248  gricushgr  48271  isubgrgrim  48283  rngcsectALTV  48629  ringcsectALTV  48663  elbigo2  48906  itsclc0b  49126  itscnhlinecirc02p  49139  pm5.32dav  49147  reuxfr1dd  49160  opndisj  49256  clddisj  49257  lubeldm2d  49311  glbeldm2d  49312  sectpropdlem  49389  uppropd  49534  initopropd  49596  termopropd  49597