Theorem pm5.32da 587

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bian1d  588  rexbidva  3183  rexbida  3273  rmobidva  3379  reubidva  3380  rmobida  3389  reubida  3390  rabbidva  3419  rabbida  3439  reuxfr1d  3712  eqrrabd  4039  mpteq12da  5182  mpteq12f  5184  mpteq12dva  5185  reuhypd  5375  xpdifid  6150  funbrfv2b  6920  dffn5  6921  feqmptdf  6933  funcnvmpt  6973  eqfnfv2  7008  fmptco  7107  dff13  7234  riotabidva  7368  mpoeq123dva  7466  mpoeq3dva  7469  opiota  8036  fnwelem  8106  suppssr  8170  mpoxopovel  8195  mpocurryd  8244  oeeui  8567  omabs  8616  eldifsucnn  8629  qliftfun  8779  erovlem  8790  mapsnend  9013  xpcomco  9035  pw2f1olem  9049  elfi2  9357  cardval2  9946  dfac2b  10084  cflim3  10216  iundom2g  10494  fpwwe2lem7  10592  fpwwe2lem11  10596  ltexpi  10857  ordpipq  10897  axrrecex  11118  nnunb  12474  zrevaddcl  12613  qrevaddcl  12969  icoshft  13474  fznn  13594  preduz  13652  predfz  13655  fznnfl  13869  fz1isolem  14471  pfxeq  14706  pfxsuffeqwrdeq  14708  pfxsuff1eqwrdeq  14709  2swrd2eqwrdeq  14963  eqwrds3  14971  2shfti  15090  limsupgle  15487  ello12  15526  elo12  15537  isercoll  15678  sumeq2ii  15703  fsum2dlem  15780  prodeq2ii  15924  bitsmod  16453  bitscmp  16455  pwsle  17505  imasleval  17554  acsfiel  17669  ismon2  17750  isepi2  17757  oppcsect  17794  subsubc  17869  funcpropd  17918  fullpropd  17938  fucsect  17991  setcsect  18105  pltval3  18352  grpidpropd  18679  ismgmid  18682  gsumpropd2lem  18696  mgmhmpropd  18715  issubmgm2  18720  mhmpropd  18809  issubm2  18821  subgacs  19185  eqgid  19204  eqg0subg  19220  ghmqusker  19310  pgpfi2  19629  eqgabl  19857  iscyggen2  19904  cyggenod  19907  eldprd  20029  subgdmdprd  20059  dprd2d2  20069  rngpropd  20203  ringpropd  20317  crngunit  20406  dvdsrpropd  20444  isrnghmmul  20470  issubrg3  20629  rngcsect  20665  ringcsect  20699  drngpropd  20798  sdrgacs  20830  lsslss  21008  lsspropd  21064  lmhmpropd  21120  lbspropd  21146  znleval  21586  znunithash  21596  pjdm2  21743  islinds2  21845  aspval2  21930  bastop2  23034  elcls2  23114  neiptopreu  23173  maxlp  23187  restopn2  23217  iscnp3  23284  subbascn  23294  lmbr2  23299  kgencn  23596  kgencn2  23597  hauseqlcld  23686  txlm  23688  txkgen  23692  xkoptsub  23694  idqtop  23746  tgqtop  23752  qtopcld  23753  elmptrab  23867  flimopn  24015  fbflim  24016  fbflim2  24017  flimrest  24023  flffbas  24035  flftg  24036  cnflf  24042  cnflf2  24043  txflf  24046  isfcls  24049  fclsopn  24054  fclsbas  24061  fclsrest  24064  fcfnei  24075  cnfcf  24082  ptcmplem2  24093  tgphaus  24157  tsmssubm  24183  isucn2  24318  ismet2  24373  xblpnfps  24435  xblpnf  24436  blin  24461  blres  24471  elmopn2  24485  imasf1obl  24528  imasf1oxms  24529  prdsbl  24531  neibl  24541  metrest  24564  metcnp3  24580  metcnp  24581  metcnp2  24582  metcn  24583  txmetcnp  24587  txmetcn  24588  metuel2  24605  metucn  24611  ngppropd  24677  cnbl0  24813  cnblcld  24814  bl2ioo  24832  xrtgioo  24847  elcncf2  24932  cncfmet  24951  nmhmcn  25162  lmmbr  25300  lmmbr2  25301  iscfil2  25308  iscau2  25319  iscau3  25320  lmclim  25345  shft2rab  25550  sca2rab  25554  mbfeqalem1  25683  mbfmulc2lem  25689  mbfmax  25691  mbfposr  25694  mbfimaopnlem  25697  mbfaddlem  25702  mbfsup  25706  mbfinf  25707  i1fmullem  25736  i1fmulclem  25744  i1fres  25747  itg1climres  25756  mbfi1fseqlem4  25760  ibllem  25806  ellimc2  25919  ellimc3  25921  limcflf  25923  cnplimc  25929  cnlimc  25930  dvreslem  25951  dvcnp2  25962  dvmulbr  25981  dvcobr  25988  cmvth  26033  dvfsumle  26063  ply1remlem  26205  fta1glem2  26209  ofmulrt  26323  plyremlem  26345  ulm2  26425  mcubic  26889  cubic2  26890  dvdsflsumcom  27229  fsumvma  27254  fsumvma2  27255  vmasum  27257  logfaclbnd  27263  dchrelbas2  27278  dchrelbas3  27279  dchrelbas4  27284  lgsquadlem1  27421  lgsquadlem2  27422  2lgslem1a  27432  eqcuts2  27856  colopp  28915  colhp  28916  umgr2v2enb1  29673  upgriswlk  29787  wspthsnwspthsnon  30062  elwwlks2on  30107  elwwlks2  30115  elwspths2spth  30116  isclwwlknx  30184  clwwlkn1  30189  clwwlkn2  30192  eupth2lems  30386  fusgr2wsp2nb  30482  numclwwlkqhash  30523  isblo2  30932  ubthlem1  31019  h2hlm  31129  pjpreeq  31547  elnlfn  32077  rmounid  32642  nfpconfp  32784  fmptcof2  32809  fdifsupp  32837  suppiniseg  32838  ressupprn  32842  fpwrelmapffslem  32884  nndiffz1  32938  cntzun  33220  cntrval2  33312  urpropd  33372  lindfpropd  33529  quslsm  33552  opprqus0g  33639  ressply1mon1p  33725  ply1degltel  33751  ply1degleel  33752  algextdeglem6  33980  smatrcl  34054  zarcls  34132  rhmpreimacnlem  34142  ismntop  34284  itgeq12dv  34584  eulerpartlemgvv  34634  orvcgteel  34726  reprinrn  34876  reprdifc  34885  dfrdg2  36107  broutsideof3  36440  isfne4b  36665  filnetlem4  36705  bj-elid6  37626  bj-imdirval3  37640  nlpineqsn  37866  uncf  38062  poimirlem23  38106  poimirlem26  38109  poimirlem27  38110  heicant  38118  cnambfre  38131  itg2gt0cn  38138  ftc1anclem5  38160  areacirclem5  38175  isdrngo3  38422  isidlc  38478  erimeq2  39226  prter3  39470  islshpsm  39568  islshpat  39605  lkrsc  39685  lfl1dim  39709  ldual1dim  39754  isat3  39895  glbconxN  39966  islln2  40099  islpln2  40124  islvol2  40168  cdlemg2cex  41179  diaglbN  41643  diblsmopel  41759  dihopelvalcpre  41836  xihopellsmN  41842  dihopellsm  41843  dihglbcpreN  41888  mapdval4N  42220  hdmapoc  42519  eluzp1  42880  fsuppind  43136  fsuppssindlem2  43138  prjspreln0  43155  ellz1  43312  rmydioph  43555  rmxdioph  43557  expdiophlem1  43562  expdioph  43564  pw2f1ocnv  43578  dnwech  43589  ordeldif  43799  ordeldifsucon  43800  ordeldif1o  43801  cantnfresb  43865  tfsconcat0i  43886  tfsconcatrev  43889  oadif1lem  43920  oadif1  43921  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  rfovcnvf1od  44544  k0004lem3  44689  pm14.123b  44966  rfcnpre1  45563  rfcnpre2  45575  rfcnpre3  45577  rfcnpre4  45578  climreeq  46153  funbrafv2b  47717  dfafn5a  47718  isuspgrim0  48480  gricushgr  48503  isubgrgrim  48515  rngcsectALTV  48861  ringcsectALTV  48895  elbigo2  49138  itsclc0b  49358  itscnhlinecirc02p  49371  pm5.32dav  49379  reuxfr1dd  49392  opndisj  49488  clddisj  49489  lubeldm2d  49543  glbeldm2d  49544  sectpropdlem  49621  uppropd  49766  initopropd  49828  termopropd  49829