Theorem pm5.32da 571

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  rexbidva  3234  rexbida  3254  reubida  3319  reubidva  3320  rmobida  3325  cbvrexdva2  3381  reuxfr4d  3645  mpteq12f  5006  reuhypd  5172  xpdifid  5862  funbrfv2b  6550  dffn5  6551  feqmptdf  6562  eqfnfv2  6626  fmptco  6712  dff13  6836  riotabidva  6951  mpoeq123dva  7044  mpoeq3dva  7047  opiota  7563  fnwelem  7628  suppssr  7662  mpoxopovel  7687  mpocurryd  7736  oeeui  8027  omabs  8072  qliftfun  8180  erovlem  8191  mapsnend  8383  xpcomco  8401  pw2f1olem  8415  elfi2  8671  cardval2  9212  dfac2b  9348  cflim3  9480  iundom2g  9758  fpwwe2lem8  9855  fpwwe2lem12  9859  ltexpi  10120  ordpipq  10160  axrrecex  10381  nnunb  11701  zrevaddcl  11838  qrevaddcl  12183  icoshft  12673  fznn  12789  preduz  12843  predfz  12846  fznnfl  13043  fz1isolem  13630  swrdeqOLD  13834  2swrdeqwrdeqOLD  13844  2swrd1eqwrdeqOLD  13845  pfxeq  13876  pfxsuffeqwrdeq  13878  pfxsuff1eqwrdeq  13879  2swrd2eqwrdeq  14175  2swrd2eqwrdeqOLD  14176  eqwrds3  14184  2shfti  14298  limsupgle  14693  ello12  14732  elo12  14743  isercoll  14883  sumeq2ii  14908  fsum2dlem  14983  prodeq2ii  15125  bitsmod  15643  bitscmp  15645  pwsle  16619  imasleval  16668  acsfiel  16795  ismon2  16874  isepi2  16881  oppcsect  16918  subsubc  16993  funcpropd  17040  fullpropd  17060  fucsect  17112  setcsect  17219  pltval3  17447  grpidpropd  17741  ismgmid  17744  gsumpropd2lem  17753  mhmpropd  17821  issubm2  17828  subgacs  18110  eqgid  18127  pgpfi2  18504  eqgabl  18725  iscyggen2  18768  cyggenod  18771  eldprd  18888  subgdmdprd  18918  dprd2d2  18928  ringpropd  19067  crngunit  19147  dvdsrpropd  19181  drngpropd  19264  issubrg3  19298  sdrgacs  19314  lsslss  19467  lsspropd  19523  lmhmpropd  19579  lbspropd  19605  aspval2  19853  znleval  20418  znunithash  20428  pjdm2  20572  islinds2  20674  bastop2  21321  elcls2  21401  neiptopreu  21460  maxlp  21474  restopn2  21504  iscnp3  21571  subbascn  21581  lmbr2  21586  kgencn  21883  kgencn2  21884  hauseqlcld  21973  txlm  21975  txkgen  21979  xkoptsub  21981  idqtop  22033  tgqtop  22039  qtopcld  22040  elmptrab  22154  flimopn  22302  fbflim  22303  fbflim2  22304  flimrest  22310  flffbas  22322  flftg  22323  cnflf  22329  cnflf2  22330  txflf  22333  isfcls  22336  fclsopn  22341  fclsbas  22348  fclsrest  22351  fcfnei  22362  cnfcf  22369  ptcmplem2  22380  tgphaus  22443  tsmssubm  22469  isucn2  22606  ismet2  22661  xblpnfps  22723  xblpnf  22724  blin  22749  blres  22759  elmopn2  22773  imasf1obl  22816  imasf1oxms  22817  prdsbl  22819  neibl  22829  metrest  22852  metcnp3  22868  metcnp  22869  metcnp2  22870  metcn  22871  txmetcnp  22875  txmetcn  22876  metuel2  22893  metucn  22899  ngppropd  22964  cnbl0  23100  cnblcld  23101  bl2ioo  23118  xrtgioo  23132  elcncf2  23216  cncfmet  23234  nmhmcn  23442  lmmbr  23579  lmmbr2  23580  iscfil2  23587  iscau2  23598  iscau3  23599  lmclim  23624  shft2rab  23827  sca2rab  23831  mbfeqalem1  23960  mbfmulc2lem  23966  mbfmax  23968  mbfposr  23971  mbfimaopnlem  23974  mbfaddlem  23979  mbfsup  23983  mbfinf  23984  i1fmullem  24013  i1fmulclem  24021  i1fres  24024  itg1climres  24033  mbfi1fseqlem4  24037  ibllem  24083  ellimc2  24193  ellimc3  24195  limcflf  24197  cnplimc  24203  cnlimc  24204  dvreslem  24225  ply1remlem  24474  fta1glem2  24478  ofmulrt  24589  plyremlem  24611  ulm2  24691  mcubic  25141  cubic2  25142  dvdsflsumcom  25482  fsumvma  25506  fsumvma2  25507  vmasum  25509  logfaclbnd  25515  dchrelbas2  25530  dchrelbas3  25531  dchrelbas4  25536  lgsquadlem1  25673  lgsquadlem2  25674  2lgslem1a  25684  colopp  26272  colhp  26273  umgr2v2enb1  27026  upgriswlk  27140  wspthsnwspthsnon  27437  elwwlks2on  27480  elwwlks2  27487  elwspths2spth  27488  isclwwlknx  27566  clwwlkn1  27572  clwwlkn2  27575  eupth2lems  27783  fusgr2wsp2nb  27883  numclwwlkqhash  27943  isblo2  28352  ubthlem1  28440  h2hlm  28551  pjpreeq  28971  elnlfn  29501  fmptcof2  30181  funcnvmpt  30191  fpwrelmapffslem  30244  nndiffz1  30285  lindfpropd  30645  smatrcl  30735  ismntop  30943  itgeq12dv  31261  eulerpartlemgvv  31311  orvcgteel  31403  reprinrn  31569  reprdifc  31578  dfrdg2  32598  broutsideof3  33145  isfne4b  33247  filnetlem4  33287  nlpineqsn  34167  uncf  34349  poimirlem23  34393  poimirlem26  34396  poimirlem27  34397  heicant  34405  cnambfre  34418  itg2gt0cn  34425  ftc1anclem5  34449  areacirclem5  34464  isdrngo3  34716  isidlc  34772  erim2  35393  prter3  35500  islshpsm  35598  islshpat  35635  lkrsc  35715  lfl1dim  35739  ldual1dim  35784  isat3  35925  glbconxN  35996  islln2  36129  islpln2  36154  islvol2  36198  cdlemg2cex  37209  diaglbN  37673  diblsmopel  37789  dihopelvalcpre  37866  xihopellsmN  37872  dihopellsm  37873  dihglbcpreN  37918  mapdval4N  38250  hdmapoc  38549  prjspreln0  38704  ellz1  38797  rmydioph  39045  rmxdioph  39047  expdiophlem1  39052  expdioph  39054  pw2f1ocnv  39068  dnwech  39082  rfovcnvf1od  39751  k0004lem3  39900  pm14.123b  40213  rfcnpre1  40732  rfcnpre2  40744  rfcnpre3  40746  rfcnpre4  40747  climreeq  41357  funbrafv2b  42796  dfafn5a  42797  isomushgr  43391  isomuspgr  43399  mgmhmpropd  43452  issubmgm2  43457  isrnghmmul  43560  rngcsect  43647  rngcsectALTV  43659  ringcsect  43698  ringcsectALTV  43722  elbigo2  44012  itsclc0b  44159  itscnhlinecirc02p  44172