Theorem pm5.32da 590

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bian1d  591  rexbidva  3186  rexbida  3276  rmobidva  3380  reubidva  3381  rmobida  3390  reubida  3391  rabbidva  3420  rabbida  3440  reuxfr1d  3711  eqrrabd  4037  mpteq12da  5192  mpteq12f  5194  mpteq12dva  5195  reuhypd  5388  xpdifid  6164  xpdifcnvepel  6165  funbrfv2b  6939  dffn5  6940  feqmptdf  6952  funcnvmpt  6992  eqfnfv2  7027  fmptco  7127  dff13  7255  riotabidva  7393  mpoeq123dva  7491  mpoeq3dva  7494  opiota  8060  fnwelem  8133  suppssr  8197  mpoxopovel  8222  mpocurryd  8271  oeeui  8594  omabs  8643  eldifsucnn  8656  qliftfun  8806  erovlem  8817  uncf  8874  mapsnend  9047  xpcomco  9069  pw2f1olem  9083  elfi2  9388  cardval2  10000  dfac2b  10137  cflim3  10268  iundom2g  10552  fpwwe2lem7  10650  fpwwe2lem11  10654  ltexpi  10915  ordpipq  10955  axrrecex  11176  nnunb  12528  zrevaddcl  12667  qrevaddcl  13025  icoshft  13530  fznn  13651  preduz  13709  predfz  13712  fznnfl  13927  fz1isolem  14530  pfxeq  14769  pfxsuffeqwrdeq  14771  pfxsuff1eqwrdeq  14772  2swrd2eqwrdeq  15030  eqwrds3  15038  2shfti  15157  limsupgle  15568  ello12  15607  elo12  15618  isercoll  15759  sumeq2ii  15784  fsum2dlem  15860  prodeq2ii  16004  bitsmod  16532  bitscmp  16534  pwsle  17584  imasleval  17633  acsfiel  17748  ismon2  17829  isepi2  17836  oppcsect  17873  subsubc  17948  funcpropd  17997  fullpropd  18017  fucsect  18070  setcsect  18184  pltval3  18431  grpidpropd  18761  ismgmid  18764  gsumpropd2lem  18787  mgmhmpropd  18806  issubmgm2  18811  mhmpropd  18906  issubm2  18918  subgacs  19290  eqgid  19311  eqg0subg  19330  ghmqusker  19420  pgpfi2  19739  eqgabl  19967  iscyggen2  20014  cyggenod  20017  eldprd  20139  subgdmdprd  20169  dprd2d2  20179  rngpropd  20315  ringpropd  20436  crngunit  20525  dvdsrpropd  20563  isrnghmmul  20589  issubrg3  20768  rngcsect  20804  ringcsect  20838  drngpropd  20942  sdrgacs  20973  lsslss  21151  lsspropd  21207  lmhmpropd  21263  lbspropd  21289  df2idl2crng  21490  znleval  21773  znunithash  21783  pjdm2  21930  islinds2  22032  aspval2  22119  bastop2  23225  elcls2  23305  neiptopreu  23364  maxlp  23378  restopn2  23408  iscnp3  23475  subbascn  23485  lmbr2  23490  kgencn  23788  kgencn2  23789  hauseqlcld  23878  txlm  23880  txkgen  23884  xkoptsub  23886  idqtop  23938  tgqtop  23944  qtopcld  23945  elmptrab  24059  flimopn  24207  fbflim  24208  fbflim2  24209  flimrest  24215  flffbas  24227  flftg  24228  cnflf  24234  cnflf2  24235  txflf  24238  isfcls  24241  fclsopn  24246  fclsbas  24253  fclsrest  24256  fcfnei  24267  cnfcf  24274  ptcmplem2  24285  tgphaus  24349  tsmssubm  24375  isucn2  24510  ismet2  24565  xblpnfps  24627  xblpnf  24628  blin  24653  blres  24663  elmopn2  24677  imasf1obl  24720  imasf1oxms  24721  prdsbl  24723  neibl  24733  metrest  24756  metcnp3  24772  metcnp  24773  metcnp2  24774  metcn  24775  txmetcnp  24779  txmetcn  24780  metuel2  24797  metucn  24803  ngppropd  24869  cnbl0  25005  cnblcld  25006  bl2ioo  25024  xrtgioo  25039  elcncf2  25124  cncfmet  25143  nmhmcn  25354  lmmbr  25492  lmmbr2  25493  iscfil2  25500  iscau2  25511  iscau3  25512  lmclim  25537  shft2rab  25742  sca2rab  25746  mbfeqalem1  25875  mbfmulc2lem  25881  mbfmax  25883  mbfposr  25886  mbfimaopnlem  25889  mbfaddlem  25894  mbfsup  25898  mbfinf  25899  i1fmullem  25928  i1fmulclem  25936  i1fres  25939  itg1climres  25948  mbfi1fseqlem4  25952  ibllem  25998  ellimc2  26111  ellimc3  26113  limcflf  26115  cnplimc  26121  cnlimc  26122  dvreslem  26143  dvcnp2  26154  dvmulbr  26173  dvcobr  26180  cmvth  26225  dvfsumle  26255  ply1remlem  26397  fta1glem2  26401  ofmulrt  26516  plyremlem  26541  rnplynfin  26546  ulm2  26628  mcubic  27092  cubic2  27093  dvdsflsumcom  27432  fsumvma  27457  fsumvma2  27458  vmasum  27460  logfaclbnd  27466  dchrelbas2  27481  dchrelbas3  27482  dchrelbas4  27487  lgsquadlem1  27624  lgsquadlem2  27625  2lgslem1a  27635  eqcuts2  28059  colopp  29134  colhp  29135  angmgmaddcpbl  29277  dfprlng2  29312  umgr2v2enb1  29994  upgriswlk  30108  wspthsnwspthsnon  30392  elwwlks2on  30437  elwwlks2  30445  elwspths2spth  30446  isclwwlknx  30514  clwwlkn1  30519  clwwlkn2  30522  eupth2lems  30726  fusgr2wsp2nb  30822  numclwwlkqhash  30863  isblo2  31272  ubthlem1  31359  h2hlm  31469  pjpreeq  31887  elnlfn  32417  rmounid  32978  nfpconfp  33113  fmptcof2  33138  fdifsupp  33165  suppiniseg  33166  ressupprn  33170  fpwrelmapffslem  33211  nndiffz1  33265  cntzun  33527  cntrval2  33619  urpropd  33678  lindfpropd  33823  quslsm  33842  opprqus0g  33900  ressply1mon1p  33986  ply1degltel  34012  ply1degleel  34013  algextdeglem6  34240  smatrcl  34314  zarcls  34392  rhmpreimacnlem  34402  ismntop  34544  itgeq12dv  34845  eulerpartlemgvv  34895  orvcgteel  34987  reprinrn  35134  reprdifc  35143  dfrdg2  36380  broutsideof3  36714  isfne4b  36968  filnetlem4  37008  bj-elid6  37930  bj-imdirval3  37944  nlpineqsn  38170  poimirlem23  38400  poimirlem26  38403  poimirlem27  38404  heicant  38412  cnambfre  38425  itg2gt0cn  38432  ftc1anclem5  38454  areacirclem5  38469  isdrngo3  38717  isidlc  38773  erimeq2  39519  prter3  39763  islshpsm  39861  islshpat  39898  lkrsc  39978  lfl1dim  40002  ldual1dim  40047  isat3  40188  glbconxN  40259  islln2  40392  islpln2  40417  islvol2  40461  cdlemg2cex  41472  diaglbN  41936  diblsmopel  42052  dihopelvalcpre  42129  xihopellsmN  42135  dihopellsm  42136  dihglbcpreN  42181  mapdval4N  42513  hdmapoc  42812  eluzp1  43190  fsuppind  43444  fsuppssindlem2  43446  prjspreln0  43463  ellz1  43620  rmydioph  43863  rmxdioph  43865  expdiophlem1  43870  expdioph  43872  pw2f1ocnv  43886  dnwech  43897  ordeldif  44107  ordeldifsucon  44108  ordeldif1o  44109  cantnfresb  44173  tfsconcat0i  44194  tfsconcatrev  44197  oadif1lem  44228  oadif1  44229  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  rfovcnvf1od  44852  k0004lem3  44997  pm14.123b  45258  rfcnpre1  45861  rfcnpre2  45873  rfcnpre3  45875  rfcnpre4  45876  climreeq  46451  funbrafv2b  48055  dfafn5a  48056  isuspgrim0  48818  gricushgr  48841  isubgrgrim  48853  rngcsectALTV  49198  ringcsectALTV  49232  elbigo2  49490  itsclc0b  49710  itscnhlinecirc02p  49723  pm5.32dav  49730  reuxfr1dd  49743  opndisj  49837  clddisj  49838  lubeldm2d  49892  glbeldm2d  49893  sectpropdlem  49970  uppropd  50115  initopropd  50177  termopropd  50178