Theorem pm5.32da 577

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  rexbidva  3174  rexbida  3267  cbvrexdva2OLD  3344  rmobidva  3389  reubidva  3390  rmobida  3400  reubida  3401  rabbidva  3437  rabbida  3456  reuxfr1d  3745  mpteq12da  5232  mpteq12f  5235  mpteq12dva  5236  reuhypd  5416  xpdifid  6166  funbrfv2b  6948  dffn5  6949  feqmptdf  6961  eqfnfv2  7032  fmptco  7128  dff13  7256  riotabidva  7387  mpoeq123dva  7485  mpoeq3dva  7488  opiota  8047  fnwelem  8119  suppssr  8183  mpoxopovel  8207  mpocurryd  8256  oeeui  8604  omabs  8652  eldifsucnn  8665  qliftfun  8798  erovlem  8809  mapsnend  9038  xpcomco  9064  pw2f1olem  9078  elfi2  9411  cardval2  9988  dfac2b  10127  cflim3  10259  iundom2g  10537  fpwwe2lem7  10634  fpwwe2lem11  10638  ltexpi  10899  ordpipq  10939  axrrecex  11160  nnunb  12472  zrevaddcl  12611  qrevaddcl  12959  icoshft  13454  fznn  13573  preduz  13627  predfz  13630  fznnfl  13831  fz1isolem  14426  pfxeq  14650  pfxsuffeqwrdeq  14652  pfxsuff1eqwrdeq  14653  2swrd2eqwrdeq  14908  eqwrds3  14916  2shfti  15031  limsupgle  15425  ello12  15464  elo12  15475  isercoll  15618  sumeq2ii  15643  fsum2dlem  15720  prodeq2ii  15861  bitsmod  16381  bitscmp  16383  pwsle  17442  imasleval  17491  acsfiel  17602  ismon2  17685  isepi2  17692  oppcsect  17729  subsubc  17807  funcpropd  17855  fullpropd  17875  fucsect  17929  setcsect  18043  pltval3  18296  grpidpropd  18587  ismgmid  18590  gsumpropd2lem  18604  mgmhmpropd  18623  issubmgm2  18628  mhmpropd  18714  issubm2  18721  subgacs  19077  eqgid  19096  eqg0subg  19111  pgpfi2  19515  eqgabl  19743  iscyggen2  19790  cyggenod  19793  eldprd  19915  subgdmdprd  19945  dprd2d2  19955  rngpropd  20068  ringpropd  20176  crngunit  20269  dvdsrpropd  20307  isrnghmmul  20333  issubrg3  20490  drngpropd  20537  sdrgacs  20560  lsslss  20716  lsspropd  20772  lmhmpropd  20828  lbspropd  20854  znleval  21329  znunithash  21339  pjdm2  21485  islinds2  21587  aspval2  21671  bastop2  22717  elcls2  22798  neiptopreu  22857  maxlp  22871  restopn2  22901  iscnp3  22968  subbascn  22978  lmbr2  22983  kgencn  23280  kgencn2  23281  hauseqlcld  23370  txlm  23372  txkgen  23376  xkoptsub  23378  idqtop  23430  tgqtop  23436  qtopcld  23437  elmptrab  23551  flimopn  23699  fbflim  23700  fbflim2  23701  flimrest  23707  flffbas  23719  flftg  23720  cnflf  23726  cnflf2  23727  txflf  23730  isfcls  23733  fclsopn  23738  fclsbas  23745  fclsrest  23748  fcfnei  23759  cnfcf  23766  ptcmplem2  23777  tgphaus  23841  tsmssubm  23867  isucn2  24004  ismet2  24059  xblpnfps  24121  xblpnf  24122  blin  24147  blres  24157  elmopn2  24171  imasf1obl  24217  imasf1oxms  24218  prdsbl  24220  neibl  24230  metrest  24253  metcnp3  24269  metcnp  24270  metcnp2  24271  metcn  24272  txmetcnp  24276  txmetcn  24277  metuel2  24294  metucn  24300  ngppropd  24366  cnbl0  24510  cnblcld  24511  bl2ioo  24528  xrtgioo  24542  elcncf2  24630  cncfmet  24649  nmhmcn  24867  lmmbr  25006  lmmbr2  25007  iscfil2  25014  iscau2  25025  iscau3  25026  lmclim  25051  shft2rab  25257  sca2rab  25261  mbfeqalem1  25390  mbfmulc2lem  25396  mbfmax  25398  mbfposr  25401  mbfimaopnlem  25404  mbfaddlem  25409  mbfsup  25413  mbfinf  25414  i1fmullem  25443  i1fmulclem  25452  i1fres  25455  itg1climres  25464  mbfi1fseqlem4  25468  ibllem  25514  ellimc2  25626  ellimc3  25628  limcflf  25630  cnplimc  25636  cnlimc  25637  dvreslem  25658  dvcnp2  25669  dvmulbr  25689  dvcobr  25697  ply1remlem  25915  fta1glem2  25919  ofmulrt  26031  plyremlem  26053  ulm2  26133  mcubic  26588  cubic2  26589  dvdsflsumcom  26928  fsumvma  26952  fsumvma2  26953  vmasum  26955  logfaclbnd  26961  dchrelbas2  26976  dchrelbas3  26977  dchrelbas4  26982  lgsquadlem1  27119  lgsquadlem2  27120  2lgslem1a  27130  eqscut2  27544  colopp  28287  colhp  28288  umgr2v2enb1  29050  upgriswlk  29165  wspthsnwspthsnon  29437  elwwlks2on  29480  elwwlks2  29487  elwspths2spth  29488  isclwwlknx  29556  clwwlkn1  29561  clwwlkn2  29564  eupth2lems  29758  fusgr2wsp2nb  29854  numclwwlkqhash  29895  isblo2  30303  ubthlem1  30390  h2hlm  30500  pjpreeq  30918  elnlfn  31448  rmounid  32002  eqrrabd  32008  nfpconfp  32123  fmptcof2  32149  funcnvmpt  32159  suppiniseg  32175  ressupprn  32179  fpwrelmapffslem  32224  nndiffz1  32264  cntzun  32482  urpropd  32648  lindfpropd  32772  quslsm  32790  ghmqusker  32806  opprqus0g  32878  ressply1mon1p  32931  ply1degltel  32940  ply1degleel  32941  algextdeglem6  33067  smatrcl  33074  zarcls  33152  rhmpreimacnlem  33162  ismntop  33304  itgeq12dv  33623  eulerpartlemgvv  33673  orvcgteel  33764  reprinrn  33928  reprdifc  33937  dfrdg2  35071  broutsideof3  35402  gg-cmvth  35466  gg-dvfsumle  35468  isfne4b  35529  filnetlem4  35569  bj-elid6  36354  bj-imdirval3  36368  nlpineqsn  36592  uncf  36770  poimirlem23  36814  poimirlem26  36817  poimirlem27  36818  heicant  36826  cnambfre  36839  itg2gt0cn  36846  ftc1anclem5  36868  areacirclem5  36883  isdrngo3  37130  isidlc  37186  erimeq2  37851  prter3  38055  islshpsm  38153  islshpat  38190  lkrsc  38270  lfl1dim  38294  ldual1dim  38339  isat3  38480  glbconxN  38552  islln2  38685  islpln2  38710  islvol2  38754  cdlemg2cex  39765  diaglbN  40229  diblsmopel  40345  dihopelvalcpre  40422  xihopellsmN  40428  dihopellsm  40429  dihglbcpreN  40474  mapdval4N  40806  hdmapoc  41105  fsuppind  41464  fsuppssindlem2  41466  prjspreln0  41653  ellz1  41807  rmydioph  42055  rmxdioph  42057  expdiophlem1  42062  expdioph  42064  pw2f1ocnv  42078  dnwech  42092  ordeldif  42310  ordeldifsucon  42311  ordeldif1o  42312  cantnfresb  42376  tfsconcat0i  42397  tfsconcatrev  42400  oadif1lem  42431  oadif1  42432  fzunt  42508  fzuntd  42509  fzunt1d  42510  fzuntgd  42511  rfovcnvf1od  43057  k0004lem3  43202  pm14.123b  43487  rfcnpre1  44005  rfcnpre2  44017  rfcnpre3  44019  rfcnpre4  44020  climreeq  44627  funbrafv2b  46165  dfafn5a  46166  isomushgr  46792  isomuspgr  46800  rngcsect  46966  rngcsectALTV  46978  ringcsect  47017  ringcsectALTV  47041  elbigo2  47325  itsclc0b  47545  itscnhlinecirc02p  47558  pm5.32dav  47566  opndisj  47622  clddisj  47623  lubeldm2d  47678  glbeldm2d  47679