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  3174  rexbida  3269  cbvrexdva2OLD  3347  rmobidva  3392  reubidva  3393  rmobida  3403  reubida  3404  rabbidva  3439  rabbida  3460  reuxfr1d  3758  eqrrabd  4095  mpteq12da  5232  mpteq12f  5235  mpteq12dva  5236  reuhypd  5424  xpdifid  6189  funbrfv2b  6965  dffn5  6966  feqmptdf  6978  eqfnfv2  7051  fmptco  7148  dff13  7274  riotabidva  7406  mpoeq123dva  7506  mpoeq3dva  7509  opiota  8082  fnwelem  8154  suppssr  8218  mpoxopovel  8243  mpocurryd  8292  oeeui  8638  omabs  8687  eldifsucnn  8700  qliftfun  8840  erovlem  8851  mapsnend  9074  xpcomco  9100  pw2f1olem  9114  elfi2  9451  cardval2  10028  dfac2b  10168  cflim3  10299  iundom2g  10577  fpwwe2lem7  10674  fpwwe2lem11  10678  ltexpi  10939  ordpipq  10979  axrrecex  11200  nnunb  12519  zrevaddcl  12659  qrevaddcl  13010  icoshft  13509  fznn  13628  preduz  13686  predfz  13689  fznnfl  13898  fz1isolem  14496  pfxeq  14730  pfxsuffeqwrdeq  14732  pfxsuff1eqwrdeq  14733  2swrd2eqwrdeq  14988  eqwrds3  14996  2shfti  15115  limsupgle  15509  ello12  15548  elo12  15559  isercoll  15700  sumeq2ii  15725  fsum2dlem  15802  prodeq2ii  15943  bitsmod  16469  bitscmp  16471  pwsle  17538  imasleval  17587  acsfiel  17698  ismon2  17781  isepi2  17788  oppcsect  17825  subsubc  17903  funcpropd  17953  fullpropd  17973  fucsect  18028  setcsect  18142  pltval3  18396  grpidpropd  18687  ismgmid  18690  gsumpropd2lem  18704  mgmhmpropd  18723  issubmgm2  18728  mhmpropd  18817  issubm2  18829  subgacs  19191  eqgid  19210  eqg0subg  19226  ghmqusker  19317  pgpfi2  19638  eqgabl  19866  iscyggen2  19913  cyggenod  19916  eldprd  20038  subgdmdprd  20068  dprd2d2  20078  rngpropd  20191  ringpropd  20301  crngunit  20394  dvdsrpropd  20432  isrnghmmul  20458  issubrg3  20616  rngcsect  20652  ringcsect  20686  drngpropd  20785  sdrgacs  20818  lsslss  20976  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  znleval  21590  znunithash  21600  pjdm2  21748  islinds2  21850  aspval2  21935  bastop2  23016  elcls2  23097  neiptopreu  23156  maxlp  23170  restopn2  23200  iscnp3  23267  subbascn  23277  lmbr2  23282  kgencn  23579  kgencn2  23580  hauseqlcld  23669  txlm  23671  txkgen  23675  xkoptsub  23677  idqtop  23729  tgqtop  23735  qtopcld  23736  elmptrab  23850  flimopn  23998  fbflim  23999  fbflim2  24000  flimrest  24006  flffbas  24018  flftg  24019  cnflf  24025  cnflf2  24026  txflf  24029  isfcls  24032  fclsopn  24037  fclsbas  24044  fclsrest  24047  fcfnei  24058  cnfcf  24065  ptcmplem2  24076  tgphaus  24140  tsmssubm  24166  isucn2  24303  ismet2  24358  xblpnfps  24420  xblpnf  24421  blin  24446  blres  24456  elmopn2  24470  imasf1obl  24516  imasf1oxms  24517  prdsbl  24519  neibl  24529  metrest  24552  metcnp3  24568  metcnp  24569  metcnp2  24570  metcn  24571  txmetcnp  24575  txmetcn  24576  metuel2  24593  metucn  24599  ngppropd  24665  cnbl0  24809  cnblcld  24810  bl2ioo  24827  xrtgioo  24841  elcncf2  24929  cncfmet  24948  nmhmcn  25166  lmmbr  25305  lmmbr2  25306  iscfil2  25313  iscau2  25324  iscau3  25325  lmclim  25350  shft2rab  25556  sca2rab  25560  mbfeqalem1  25689  mbfmulc2lem  25695  mbfmax  25697  mbfposr  25700  mbfimaopnlem  25703  mbfaddlem  25708  mbfsup  25712  mbfinf  25713  i1fmullem  25742  i1fmulclem  25751  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  ibllem  25813  ellimc2  25926  ellimc3  25928  limcflf  25930  cnplimc  25936  cnlimc  25937  dvreslem  25958  dvcnp2  25969  dvmulbr  25989  dvcobr  25997  cmvth  26043  dvfsumle  26074  ply1remlem  26218  fta1glem2  26222  ofmulrt  26337  plyremlem  26360  ulm2  26442  mcubic  26904  cubic2  26905  dvdsflsumcom  27245  fsumvma  27271  fsumvma2  27272  vmasum  27274  logfaclbnd  27280  dchrelbas2  27295  dchrelbas3  27296  dchrelbas4  27301  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a  27449  eqscut2  27865  colopp  28791  colhp  28792  umgr2v2enb1  29558  upgriswlk  29673  wspthsnwspthsnon  29945  elwwlks2on  29988  elwwlks2  29995  elwspths2spth  29996  isclwwlknx  30064  clwwlkn1  30069  clwwlkn2  30072  eupth2lems  30266  fusgr2wsp2nb  30362  numclwwlkqhash  30403  isblo2  30811  ubthlem1  30898  h2hlm  31008  pjpreeq  31426  elnlfn  31956  rmounid  32522  nfpconfp  32648  fmptcof2  32673  funcnvmpt  32683  fdifsupp  32699  suppiniseg  32700  ressupprn  32704  fpwrelmapffslem  32749  nndiffz1  32794  cntzun  33053  urpropd  33221  lindfpropd  33389  quslsm  33412  opprqus0g  33497  ressply1mon1p  33572  ply1degltel  33594  ply1degleel  33595  algextdeglem6  33727  smatrcl  33756  zarcls  33834  rhmpreimacnlem  33844  ismntop  33988  itgeq12dv  34307  eulerpartlemgvv  34357  orvcgteel  34448  reprinrn  34611  reprdifc  34620  dfrdg2  35776  broutsideof3  36107  isfne4b  36323  filnetlem4  36363  bj-elid6  37152  bj-imdirval3  37166  nlpineqsn  37390  uncf  37585  poimirlem23  37629  poimirlem26  37632  poimirlem27  37633  heicant  37641  cnambfre  37654  itg2gt0cn  37661  ftc1anclem5  37683  areacirclem5  37698  isdrngo3  37945  isidlc  38001  erimeq2  38659  prter3  38863  islshpsm  38961  islshpat  38998  lkrsc  39078  lfl1dim  39102  ldual1dim  39147  isat3  39288  glbconxN  39360  islln2  39493  islpln2  39518  islvol2  39562  cdlemg2cex  40573  diaglbN  41037  diblsmopel  41153  dihopelvalcpre  41230  xihopellsmN  41236  dihopellsm  41237  dihglbcpreN  41282  mapdval4N  41614  hdmapoc  41913  eluzp1  42319  fsuppind  42576  fsuppssindlem2  42578  prjspreln0  42595  ellz1  42754  rmydioph  43002  rmxdioph  43004  expdiophlem1  43009  expdioph  43011  pw2f1ocnv  43025  dnwech  43036  ordeldif  43247  ordeldifsucon  43248  ordeldif1o  43249  cantnfresb  43313  tfsconcat0i  43334  tfsconcatrev  43337  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rfovcnvf1od  43993  k0004lem3  44138  pm14.123b  44421  rfcnpre1  44956  rfcnpre2  44968  rfcnpre3  44970  rfcnpre4  44971  climreeq  45568  funbrafv2b  47108  dfafn5a  47109  isuspgrim0  47809  gricushgr  47823  isubgrgrim  47834  rngcsectALTV  48118  ringcsectALTV  48152  elbigo2  48401  itsclc0b  48621  itscnhlinecirc02p  48634  pm5.32dav  48642  reuxfr1dd  48654  opndisj  48698  clddisj  48699  lubeldm2d  48754  glbeldm2d  48755