Theorem pm5.32da 578

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 576	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  rexbidva  3224  rexbida  3246  reubida  3313  reubidva  3314  rmobida  3318  cbvrexdva2  3382  rabbidva  3402  reuxfr1d  3680  mpteq12da  5155  mpteq12f  5158  mpteq12dva  5159  reuhypd  5337  xpdifid  6060  funbrfv2b  6809  dffn5  6810  feqmptdf  6821  eqfnfv2  6892  fmptco  6983  dff13  7109  riotabidva  7232  mpoeq123dva  7327  mpoeq3dva  7330  opiota  7872  fnwelem  7943  suppssr  7983  mpoxopovel  8007  mpocurryd  8056  oeeui  8395  omabs  8441  qliftfun  8549  erovlem  8560  mapsnend  8780  xpcomco  8802  pw2f1olem  8816  elfi2  9103  cardval2  9680  dfac2b  9817  cflim3  9949  iundom2g  10227  fpwwe2lem7  10324  fpwwe2lem11  10328  ltexpi  10589  ordpipq  10629  axrrecex  10850  nnunb  12159  zrevaddcl  12295  qrevaddcl  12640  icoshft  13134  fznn  13253  preduz  13307  predfz  13310  fznnfl  13510  fz1isolem  14103  pfxeq  14337  pfxsuffeqwrdeq  14339  pfxsuff1eqwrdeq  14340  2swrd2eqwrdeq  14594  eqwrds3  14604  2shfti  14719  limsupgle  15114  ello12  15153  elo12  15164  isercoll  15307  sumeq2ii  15333  fsum2dlem  15410  prodeq2ii  15551  bitsmod  16071  bitscmp  16073  pwsle  17120  imasleval  17169  acsfiel  17280  ismon2  17363  isepi2  17370  oppcsect  17407  subsubc  17484  funcpropd  17532  fullpropd  17552  fucsect  17606  setcsect  17720  pltval3  17972  grpidpropd  18261  ismgmid  18264  gsumpropd2lem  18278  mhmpropd  18351  issubm2  18358  subgacs  18704  eqgid  18723  pgpfi2  19126  eqgabl  19351  iscyggen2  19396  cyggenod  19399  eldprd  19522  subgdmdprd  19552  dprd2d2  19562  ringpropd  19736  crngunit  19819  dvdsrpropd  19853  drngpropd  19933  issubrg3  19967  sdrgacs  19984  lsslss  20138  lsspropd  20194  lmhmpropd  20250  lbspropd  20276  znleval  20674  znunithash  20684  pjdm2  20828  islinds2  20930  aspval2  21012  bastop2  22052  elcls2  22133  neiptopreu  22192  maxlp  22206  restopn2  22236  iscnp3  22303  subbascn  22313  lmbr2  22318  kgencn  22615  kgencn2  22616  hauseqlcld  22705  txlm  22707  txkgen  22711  xkoptsub  22713  idqtop  22765  tgqtop  22771  qtopcld  22772  elmptrab  22886  flimopn  23034  fbflim  23035  fbflim2  23036  flimrest  23042  flffbas  23054  flftg  23055  cnflf  23061  cnflf2  23062  txflf  23065  isfcls  23068  fclsopn  23073  fclsbas  23080  fclsrest  23083  fcfnei  23094  cnfcf  23101  ptcmplem2  23112  tgphaus  23176  tsmssubm  23202  isucn2  23339  ismet2  23394  xblpnfps  23456  xblpnf  23457  blin  23482  blres  23492  elmopn2  23506  imasf1obl  23550  imasf1oxms  23551  prdsbl  23553  neibl  23563  metrest  23586  metcnp3  23602  metcnp  23603  metcnp2  23604  metcn  23605  txmetcnp  23609  txmetcn  23610  metuel2  23627  metucn  23633  ngppropd  23699  cnbl0  23843  cnblcld  23844  bl2ioo  23861  xrtgioo  23875  elcncf2  23959  cncfmet  23978  nmhmcn  24189  lmmbr  24327  lmmbr2  24328  iscfil2  24335  iscau2  24346  iscau3  24347  lmclim  24372  shft2rab  24577  sca2rab  24581  mbfeqalem1  24710  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  mbfimaopnlem  24724  mbfaddlem  24729  mbfsup  24733  mbfinf  24734  i1fmullem  24763  i1fmulclem  24772  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  ibllem  24834  ellimc2  24946  ellimc3  24948  limcflf  24950  cnplimc  24956  cnlimc  24957  dvreslem  24978  ply1remlem  25232  fta1glem2  25236  ofmulrt  25347  plyremlem  25369  ulm2  25449  mcubic  25902  cubic2  25903  dvdsflsumcom  26242  fsumvma  26266  fsumvma2  26267  vmasum  26269  logfaclbnd  26275  dchrelbas2  26290  dchrelbas3  26291  dchrelbas4  26296  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1a  26444  colopp  27034  colhp  27035  umgr2v2enb1  27796  upgriswlk  27910  wspthsnwspthsnon  28182  elwwlks2on  28225  elwwlks2  28232  elwspths2spth  28233  isclwwlknx  28301  clwwlkn1  28306  clwwlkn2  28309  eupth2lems  28503  fusgr2wsp2nb  28599  numclwwlkqhash  28640  isblo2  29046  ubthlem1  29133  h2hlm  29243  pjpreeq  29661  elnlfn  30191  rmounid  30744  eqrrabd  30750  nfpconfp  30868  fmptcof2  30896  funcnvmpt  30906  suppiniseg  30922  ressupprn  30926  fpwrelmapffslem  30969  nndiffz1  31009  cntzun  31222  lindfpropd  31478  quslsm  31495  smatrcl  31648  zarcls  31726  rhmpreimacnlem  31736  ismntop  31876  itgeq12dv  32193  eulerpartlemgvv  32243  orvcgteel  32334  reprinrn  32498  reprdifc  32507  eldifsucnn  33597  dfrdg2  33677  eqscut2  33927  broutsideof3  34355  isfne4b  34457  filnetlem4  34497  bj-elid6  35268  bj-imdirval3  35282  nlpineqsn  35506  uncf  35683  poimirlem23  35727  poimirlem26  35730  poimirlem27  35731  heicant  35739  cnambfre  35752  itg2gt0cn  35759  ftc1anclem5  35781  areacirclem5  35796  isdrngo3  36044  isidlc  36100  erim2  36716  prter3  36823  islshpsm  36921  islshpat  36958  lkrsc  37038  lfl1dim  37062  ldual1dim  37107  isat3  37248  glbconxN  37319  islln2  37452  islpln2  37477  islvol2  37521  cdlemg2cex  38532  diaglbN  38996  diblsmopel  39112  dihopelvalcpre  39189  xihopellsmN  39195  dihopellsm  39196  dihglbcpreN  39241  mapdval4N  39573  hdmapoc  39872  fsuppind  40202  fsuppssindlem2  40204  prjspreln0  40369  ellz1  40505  rmydioph  40752  rmxdioph  40754  expdiophlem1  40759  expdioph  40761  pw2f1ocnv  40775  dnwech  40789  rfovcnvf1od  41501  k0004lem3  41648  pm14.123b  41933  rfcnpre1  42451  rfcnpre2  42463  rfcnpre3  42465  rfcnpre4  42466  climreeq  43044  funbrafv2b  44538  dfafn5a  44539  isomushgr  45166  isomuspgr  45174  mgmhmpropd  45227  issubmgm2  45232  isrnghmmul  45339  rngcsect  45426  rngcsectALTV  45438  ringcsect  45477  ringcsectALTV  45501  elbigo2  45786  itsclc0b  46006  itscnhlinecirc02p  46019  pm5.32dav  46027  opndisj  46084  clddisj  46085  lubeldm2d  46140  glbeldm2d  46141