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:  rexbidva  3155  rexbida  3245  rmobidva  3360  reubidva  3361  rmobida  3370  reubida  3371  rabbidva  3402  rabbida  3422  reuxfr1d  3705  eqrrabd  4035  mpteq12da  5176  mpteq12f  5178  mpteq12dva  5179  reuhypd  5359  xpdifid  6120  funbrfv2b  6885  dffn5  6886  feqmptdf  6898  eqfnfv2  6971  fmptco  7068  dff13  7194  riotabidva  7328  mpoeq123dva  7426  mpoeq3dva  7429  opiota  7997  fnwelem  8067  suppssr  8131  mpoxopovel  8156  mpocurryd  8205  oeeui  8523  omabs  8572  eldifsucnn  8585  qliftfun  8732  erovlem  8743  mapsnend  8965  xpcomco  8987  pw2f1olem  9001  elfi2  9305  cardval2  9891  dfac2b  10029  cflim3  10160  iundom2g  10438  fpwwe2lem7  10535  fpwwe2lem11  10539  ltexpi  10800  ordpipq  10840  axrrecex  11061  nnunb  12384  zrevaddcl  12523  qrevaddcl  12871  icoshft  13375  fznn  13494  preduz  13552  predfz  13555  fznnfl  13768  fz1isolem  14370  pfxeq  14605  pfxsuffeqwrdeq  14607  pfxsuff1eqwrdeq  14608  2swrd2eqwrdeq  14862  eqwrds3  14870  2shfti  14989  limsupgle  15386  ello12  15425  elo12  15436  isercoll  15577  sumeq2ii  15602  fsum2dlem  15679  prodeq2ii  15820  bitsmod  16349  bitscmp  16351  pwsle  17398  imasleval  17447  acsfiel  17562  ismon2  17643  isepi2  17650  oppcsect  17687  subsubc  17762  funcpropd  17811  fullpropd  17831  fucsect  17884  setcsect  17998  pltval3  18245  grpidpropd  18572  ismgmid  18575  gsumpropd2lem  18589  mgmhmpropd  18608  issubmgm2  18613  mhmpropd  18702  issubm2  18714  subgacs  19075  eqgid  19094  eqg0subg  19110  ghmqusker  19201  pgpfi2  19520  eqgabl  19748  iscyggen2  19795  cyggenod  19798  eldprd  19920  subgdmdprd  19950  dprd2d2  19960  rngpropd  20094  ringpropd  20208  crngunit  20298  dvdsrpropd  20336  isrnghmmul  20362  issubrg3  20517  rngcsect  20553  ringcsect  20587  drngpropd  20686  sdrgacs  20718  lsslss  20896  lsspropd  20953  lmhmpropd  21009  lbspropd  21035  znleval  21493  znunithash  21503  pjdm2  21650  islinds2  21752  aspval2  21837  bastop2  22910  elcls2  22990  neiptopreu  23049  maxlp  23063  restopn2  23093  iscnp3  23160  subbascn  23170  lmbr2  23175  kgencn  23472  kgencn2  23473  hauseqlcld  23562  txlm  23564  txkgen  23568  xkoptsub  23570  idqtop  23622  tgqtop  23628  qtopcld  23629  elmptrab  23743  flimopn  23891  fbflim  23892  fbflim2  23893  flimrest  23899  flffbas  23911  flftg  23912  cnflf  23918  cnflf2  23919  txflf  23922  isfcls  23925  fclsopn  23930  fclsbas  23937  fclsrest  23940  fcfnei  23951  cnfcf  23958  ptcmplem2  23969  tgphaus  24033  tsmssubm  24059  isucn2  24194  ismet2  24249  xblpnfps  24311  xblpnf  24312  blin  24337  blres  24347  elmopn2  24361  imasf1obl  24404  imasf1oxms  24405  prdsbl  24407  neibl  24417  metrest  24440  metcnp3  24456  metcnp  24457  metcnp2  24458  metcn  24459  txmetcnp  24463  txmetcn  24464  metuel2  24481  metucn  24487  ngppropd  24553  cnbl0  24689  cnblcld  24690  bl2ioo  24708  xrtgioo  24723  elcncf2  24811  cncfmet  24830  nmhmcn  25048  lmmbr  25186  lmmbr2  25187  iscfil2  25194  iscau2  25205  iscau3  25206  lmclim  25231  shft2rab  25437  sca2rab  25441  mbfeqalem1  25570  mbfmulc2lem  25576  mbfmax  25578  mbfposr  25581  mbfimaopnlem  25584  mbfaddlem  25589  mbfsup  25593  mbfinf  25594  i1fmullem  25623  i1fmulclem  25631  i1fres  25634  itg1climres  25643  mbfi1fseqlem4  25647  ibllem  25693  ellimc2  25806  ellimc3  25808  limcflf  25810  cnplimc  25816  cnlimc  25817  dvreslem  25838  dvcnp2  25849  dvmulbr  25869  dvcobr  25877  cmvth  25923  dvfsumle  25954  ply1remlem  26098  fta1glem2  26102  ofmulrt  26217  plyremlem  26240  ulm2  26322  mcubic  26785  cubic2  26786  dvdsflsumcom  27126  fsumvma  27152  fsumvma2  27153  vmasum  27155  logfaclbnd  27161  dchrelbas2  27176  dchrelbas3  27177  dchrelbas4  27182  lgsquadlem1  27319  lgsquadlem2  27320  2lgslem1a  27330  eqscut2  27748  colopp  28748  colhp  28749  umgr2v2enb1  29507  upgriswlk  29621  wspthsnwspthsnon  29896  elwwlks2on  29941  elwwlks2  29949  elwspths2spth  29950  isclwwlknx  30018  clwwlkn1  30023  clwwlkn2  30026  eupth2lems  30220  fusgr2wsp2nb  30316  numclwwlkqhash  30357  isblo2  30765  ubthlem1  30852  h2hlm  30962  pjpreeq  31380  elnlfn  31910  rmounid  32476  nfpconfp  32616  fmptcof2  32641  funcnvmpt  32651  fdifsupp  32670  suppiniseg  32671  ressupprn  32675  fpwrelmapffslem  32719  nndiffz1  32773  cntzun  33055  cntrval2  33147  urpropd  33206  lindfpropd  33354  quslsm  33377  opprqus0g  33462  ressply1mon1p  33538  ply1degltel  33562  ply1degleel  33563  algextdeglem6  33756  smatrcl  33830  zarcls  33908  rhmpreimacnlem  33918  ismntop  34060  itgeq12dv  34360  eulerpartlemgvv  34410  orvcgteel  34502  reprinrn  34652  reprdifc  34661  dfrdg2  35858  broutsideof3  36191  isfne4b  36406  filnetlem4  36446  bj-elid6  37235  bj-imdirval3  37249  nlpineqsn  37473  uncf  37659  poimirlem23  37703  poimirlem26  37706  poimirlem27  37707  heicant  37715  cnambfre  37728  itg2gt0cn  37735  ftc1anclem5  37757  areacirclem5  37772  isdrngo3  38019  isidlc  38075  erimeq2  38796  prter3  39001  islshpsm  39099  islshpat  39136  lkrsc  39216  lfl1dim  39240  ldual1dim  39285  isat3  39426  glbconxN  39497  islln2  39630  islpln2  39655  islvol2  39699  cdlemg2cex  40710  diaglbN  41174  diblsmopel  41290  dihopelvalcpre  41367  xihopellsmN  41373  dihopellsm  41374  dihglbcpreN  41419  mapdval4N  41751  hdmapoc  42050  eluzp1  42425  fsuppind  42708  fsuppssindlem2  42710  prjspreln0  42727  ellz1  42884  rmydioph  43131  rmxdioph  43133  expdiophlem1  43138  expdioph  43140  pw2f1ocnv  43154  dnwech  43165  ordeldif  43375  ordeldifsucon  43376  ordeldif1o  43377  cantnfresb  43441  tfsconcat0i  43462  tfsconcatrev  43465  oadif1lem  43496  oadif1  43497  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  rfovcnvf1od  44121  k0004lem3  44266  pm14.123b  44543  rfcnpre1  45140  rfcnpre2  45152  rfcnpre3  45154  rfcnpre4  45155  climreeq  45737  funbrafv2b  47283  dfafn5a  47284  isuspgrim0  48018  gricushgr  48041  isubgrgrim  48053  rngcsectALTV  48399  ringcsectALTV  48433  elbigo2  48677  itsclc0b  48897  itscnhlinecirc02p  48910  pm5.32dav  48918  reuxfr1dd  48931  opndisj  49027  clddisj  49028  lubeldm2d  49082  glbeldm2d  49083  sectpropdlem  49161  uppropd  49306  initopropd  49368  termopropd  49369