Theorem pm5.32da 671

Description: Distribution of implication over biconditional (deduction rule). (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 449	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 669	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  rexbida  3029  rexbidva  3031  reubida  3101  rmobida  3106  mpteq12f  4661  reuhypd  4821  xpdifid  5481  funbrfv2b  6150  dffn5  6151  feqmptdf  6161  eqfnfv2  6220  fmptco  6303  dff13  6416  riotabidva  6527  mpt2eq123dva  6614  mpt2eq3dva  6617  opiota  7118  fnwelem  7179  suppssr  7213  mpt2xopovel  7233  mpt2curryd  7282  oeeui  7569  omabs  7614  qliftfun  7719  erovlem  7730  xpcomco  7935  pw2f1olem  7949  elfi2  8203  cardval2  8700  dfac2  8836  cflim3  8967  iundom2g  9241  fpwwe2lem8  9338  fpwwe2lem12  9342  ltexpi  9603  ordpipq  9643  axrrecex  9863  nnunb  11165  zrevaddcl  11299  qrevaddcl  11686  icoshft  12165  fznn  12278  preduz  12330  predfz  12333  fznnfl  12523  fz1isolem  13102  swrdeq  13296  2swrdeqwrdeq  13305  2swrd1eqwrdeq  13306  2swrd2eqwrdeq  13544  eqwrds3  13552  2shfti  13668  limsupgle  14056  ello12  14095  elo12  14106  isercoll  14246  sumeq2ii  14271  fsum2dlem  14343  prodeq2ii  14482  bitsmod  14996  bitscmp  14998  pwsle  15975  imasleval  16024  acsfiel  16138  ismon2  16217  isepi2  16224  oppcsect  16261  subsubc  16336  funcpropd  16383  fullpropd  16403  fucsect  16455  setcsect  16562  pltval3  16790  grpidpropd  17084  ismgmid  17087  gsumpropd2lem  17096  mhmpropd  17164  issubm2  17171  subgacs  17452  eqgid  17469  pgpfi2  17844  eqgabl  18063  iscyggen2  18106  cyggenod  18109  eldprd  18226  subgdmdprd  18256  dprd2d2  18266  ringpropd  18405  crngunit  18485  dvdsrpropd  18519  drngpropd  18597  issubrg3  18631  lsslss  18782  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  aspval2  19168  znleval  19722  znunithash  19732  pjdm2  19874  islinds2  19971  bastop2  20609  elcls2  20688  neiptopreu  20747  maxlp  20761  restopn2  20791  iscnp3  20858  subbascn  20868  lmbr2  20873  kgencn  21169  kgencn2  21170  hauseqlcld  21259  txlm  21261  txkgen  21265  xkoptsub  21267  idqtop  21319  tgqtop  21325  qtopcld  21326  elmptrab  21440  flimopn  21589  fbflim  21590  fbflim2  21591  flimrest  21597  flffbas  21609  flftg  21610  cnflf  21616  cnflf2  21617  txflf  21620  isfcls  21623  fclsopn  21628  fclsbas  21635  fclsrest  21638  fcfnei  21649  cnfcf  21656  ptcmplem2  21667  tgphaus  21730  tsmssubm  21756  isucn2  21893  ismet2  21948  xblpnfps  22010  xblpnf  22011  blin  22036  blres  22046  elmopn2  22060  imasf1obl  22103  imasf1oxms  22104  prdsbl  22106  neibl  22116  metrest  22139  metcnp3  22155  metcnp  22156  metcnp2  22157  metcn  22158  txmetcnp  22162  txmetcn  22163  metuel2  22180  metucn  22186  ngppropd  22251  cnbl0  22387  cnblcld  22388  bl2ioo  22403  xrtgioo  22417  elcncf2  22501  cncfmet  22519  nmhmcn  22728  lmmbr  22864  lmmbr2  22865  iscfil2  22872  iscau2  22883  iscau3  22884  lmclim  22909  shft2rab  23083  sca2rab  23087  mbfeqalem  23215  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  mbfimaopnlem  23228  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  i1fmullem  23267  i1fmulclem  23275  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  ibllem  23337  ellimc2  23447  ellimc3  23449  limcflf  23451  cnplimc  23457  cnlimc  23458  dvreslem  23479  ply1remlem  23726  fta1glem2  23730  ofmulrt  23841  plyremlem  23863  ulm2  23943  mcubic  24374  cubic2  24375  dvdsflsumcom  24714  fsumvma  24738  fsumvma2  24739  vmasum  24741  logfaclbnd  24747  dchrelbas2  24762  dchrelbas3  24763  dchrelbas4  24768  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a  24916  colopp  25461  colhp  25462  nbgrael  25955  nbcusgra  25992  clwwlkn2  26303  el2wlkonotot1  26401  usg2spthonot0  26416  eupath2  26507  isblo2  27022  ubthlem1  27110  h2hlm  27221  pjpreeq  27641  elnlfn  28171  reuxfr4d  28714  fmptcof2  28839  funcnvmpt  28851  fpwrelmapffslem  28895  nndiffz1  28936  smatrcl  29190  ismntop  29398  itgeq12dv  29715  eulerpartlemgvv  29765  orvcgteel  29856  dfrdg2  30945  broutsideof3  31403  isfne4b  31506  filnetlem4  31546  uncf  32558  poimirlem23  32602  poimirlem26  32605  poimirlem27  32606  heicant  32614  cnambfre  32628  itg2gt0cn  32635  ftc1anclem5  32659  areacirclem5  32674  isdrngo3  32928  isidlc  32984  prter3  33185  islshpsm  33285  islshpat  33322  lkrsc  33402  lfl1dim  33426  ldual1dim  33471  isat3  33612  glbconxN  33682  islln2  33815  islpln2  33840  islvol2  33884  cdlemg2cex  34897  diaglbN  35362  diblsmopel  35478  dihopelvalcpre  35555  xihopellsmN  35561  dihopellsm  35562  dihglbcpreN  35607  mapdval4N  35939  hdmapoc  36241  ellz1  36348  rmydioph  36599  rmxdioph  36601  expdiophlem1  36606  expdioph  36608  pw2f1ocnv  36622  dnwech  36636  sdrgacs  36790  rfovcnvf1od  37318  k0004lem3  37467  pm14.123b  37649  rfcnpre1  38201  rfcnpre2  38213  rfcnpre3  38215  rfcnpre4  38216  climreeq  38680  funbrafv2b  39888  dfafn5a  39889  pfxeq  40267  pfxsuffeqwrdeq  40269  pfxsuff1eqwrdeq  40270  nbgrel  40564  umgr2v2enb1  40742  wspthsnwspthsnon  41122  elwwlks2on  41162  elwwlks2  41170  elwspths2spth  41171  isclwwlksnx  41197  clwwlksn2  41217  eupth2lems  41406  mgmhmpropd  41575  issubmgm2  41580  isrnghmmul  41683  rngcsect  41772  rngcsectALTV  41784  ringcsect  41823  ringcsectALTV  41847  elbigo2  42144