Theorem pm5.32da 589

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bian1d  590  rexbidva  3187  rexbida  3277  rmobidva  3382  reubidva  3383  rmobida  3392  reubida  3393  rabbidva  3422  rabbida  3442  reuxfr1d  3714  eqrrabd  4041  mpteq12da  5195  mpteq12f  5197  mpteq12dva  5198  reuhypd  5392  xpdifid  6167  xpdifcnvepel  6168  funbrfv2b  6940  dffn5  6941  feqmptdf  6953  funcnvmpt  6993  eqfnfv2  7028  fmptco  7127  dff13  7254  riotabidva  7388  mpoeq123dva  7486  mpoeq3dva  7489  opiota  8057  fnwelem  8128  suppssr  8192  mpoxopovel  8217  mpocurryd  8266  oeeui  8589  omabs  8638  eldifsucnn  8651  qliftfun  8801  erovlem  8812  mapsnend  9034  xpcomco  9056  pw2f1olem  9070  elfi2  9375  cardval2  9978  dfac2b  10115  cflim3  10247  iundom2g  10525  fpwwe2lem7  10623  fpwwe2lem11  10627  ltexpi  10888  ordpipq  10928  axrrecex  11149  nnunb  12501  zrevaddcl  12640  qrevaddcl  12996  icoshft  13501  fznn  13622  preduz  13680  predfz  13683  fznnfl  13897  fz1isolem  14500  pfxeq  14735  pfxsuffeqwrdeq  14737  pfxsuff1eqwrdeq  14738  2swrd2eqwrdeq  14992  eqwrds3  15000  2shfti  15119  limsupgle  15530  ello12  15569  elo12  15580  isercoll  15721  sumeq2ii  15746  fsum2dlem  15823  prodeq2ii  15967  bitsmod  16495  bitscmp  16497  pwsle  17547  imasleval  17596  acsfiel  17711  ismon2  17792  isepi2  17799  oppcsect  17836  subsubc  17911  funcpropd  17960  fullpropd  17980  fucsect  18033  setcsect  18147  pltval3  18394  grpidpropd  18721  ismgmid  18724  gsumpropd2lem  18738  mgmhmpropd  18757  issubmgm2  18762  mhmpropd  18851  issubm2  18863  subgacs  19228  eqgid  19249  eqg0subg  19268  ghmqusker  19358  pgpfi2  19677  eqgabl  19905  iscyggen2  19952  cyggenod  19955  eldprd  20077  subgdmdprd  20107  dprd2d2  20117  rngpropd  20253  ringpropd  20372  crngunit  20461  dvdsrpropd  20499  isrnghmmul  20525  issubrg3  20686  rngcsect  20722  ringcsect  20756  drngpropd  20854  sdrgacs  20885  lsslss  21063  lsspropd  21119  lmhmpropd  21175  lbspropd  21201  df2idl2crng  21402  znleval  21685  znunithash  21695  pjdm2  21842  islinds2  21944  aspval2  22029  bastop2  23132  elcls2  23212  neiptopreu  23271  maxlp  23285  restopn2  23315  iscnp3  23382  subbascn  23392  lmbr2  23397  kgencn  23694  kgencn2  23695  hauseqlcld  23784  txlm  23786  txkgen  23790  xkoptsub  23792  idqtop  23844  tgqtop  23850  qtopcld  23851  elmptrab  23965  flimopn  24113  fbflim  24114  fbflim2  24115  flimrest  24121  flffbas  24133  flftg  24134  cnflf  24140  cnflf2  24141  txflf  24144  isfcls  24147  fclsopn  24152  fclsbas  24159  fclsrest  24162  fcfnei  24173  cnfcf  24180  ptcmplem2  24191  tgphaus  24255  tsmssubm  24281  isucn2  24416  ismet2  24471  xblpnfps  24533  xblpnf  24534  blin  24559  blres  24569  elmopn2  24583  imasf1obl  24626  imasf1oxms  24627  prdsbl  24629  neibl  24639  metrest  24662  metcnp3  24678  metcnp  24679  metcnp2  24680  metcn  24681  txmetcnp  24685  txmetcn  24686  metuel2  24703  metucn  24709  ngppropd  24775  cnbl0  24911  cnblcld  24912  bl2ioo  24930  xrtgioo  24945  elcncf2  25030  cncfmet  25049  nmhmcn  25260  lmmbr  25398  lmmbr2  25399  iscfil2  25406  iscau2  25417  iscau3  25418  lmclim  25443  shft2rab  25648  sca2rab  25652  mbfeqalem1  25781  mbfmulc2lem  25787  mbfmax  25789  mbfposr  25792  mbfimaopnlem  25795  mbfaddlem  25800  mbfsup  25804  mbfinf  25805  i1fmullem  25834  i1fmulclem  25842  i1fres  25845  itg1climres  25854  mbfi1fseqlem4  25858  ibllem  25904  ellimc2  26017  ellimc3  26019  limcflf  26021  cnplimc  26027  cnlimc  26028  dvreslem  26049  dvcnp2  26060  dvmulbr  26079  dvcobr  26086  cmvth  26131  dvfsumle  26161  ply1remlem  26303  fta1glem2  26307  ofmulrt  26421  plyremlem  26446  ulm2  26529  mcubic  26993  cubic2  26994  dvdsflsumcom  27333  fsumvma  27358  fsumvma2  27359  vmasum  27361  logfaclbnd  27367  dchrelbas2  27382  dchrelbas3  27383  dchrelbas4  27388  lgsquadlem1  27525  lgsquadlem2  27526  2lgslem1a  27536  eqcuts2  27960  colopp  29032  colhp  29033  dfprlng2  29178  umgr2v2enb1  29857  upgriswlk  29971  wspthsnwspthsnon  30246  elwwlks2on  30291  elwwlks2  30299  elwspths2spth  30300  isclwwlknx  30368  clwwlkn1  30373  clwwlkn2  30376  eupth2lems  30570  fusgr2wsp2nb  30666  numclwwlkqhash  30707  isblo2  31116  ubthlem1  31203  h2hlm  31313  pjpreeq  31731  elnlfn  32261  rmounid  32822  nfpconfp  32958  fmptcof2  32983  fdifsupp  33011  suppiniseg  33012  ressupprn  33016  fpwrelmapffslem  33058  nndiffz1  33112  cntzun  33380  cntrval2  33472  urpropd  33531  lindfpropd  33676  quslsm  33695  opprqus0g  33753  ressply1mon1p  33839  ply1degltel  33865  ply1degleel  33866  algextdeglem6  34093  smatrcl  34167  zarcls  34245  rhmpreimacnlem  34255  ismntop  34397  itgeq12dv  34697  eulerpartlemgvv  34747  orvcgteel  34839  reprinrn  34986  reprdifc  34995  dfrdg2  36266  broutsideof3  36599  isfne4b  36833  filnetlem4  36873  bj-elid6  37795  bj-imdirval3  37809  nlpineqsn  38035  uncf  38231  poimirlem23  38275  poimirlem26  38278  poimirlem27  38279  heicant  38287  cnambfre  38300  itg2gt0cn  38307  ftc1anclem5  38329  areacirclem5  38344  isdrngo3  38591  isidlc  38647  erimeq2  39393  prter3  39637  islshpsm  39735  islshpat  39772  lkrsc  39852  lfl1dim  39876  ldual1dim  39921  isat3  40062  glbconxN  40133  islln2  40266  islpln2  40291  islvol2  40335  cdlemg2cex  41346  diaglbN  41810  diblsmopel  41926  dihopelvalcpre  42003  xihopellsmN  42009  dihopellsm  42010  dihglbcpreN  42055  mapdval4N  42387  hdmapoc  42686  eluzp1  43049  fsuppind  43305  fsuppssindlem2  43307  prjspreln0  43324  ellz1  43481  rmydioph  43724  rmxdioph  43726  expdiophlem1  43731  expdioph  43733  pw2f1ocnv  43747  dnwech  43758  ordeldif  43968  ordeldifsucon  43969  ordeldif1o  43970  cantnfresb  44034  tfsconcat0i  44055  tfsconcatrev  44058  oadif1lem  44089  oadif1  44090  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  rfovcnvf1od  44713  k0004lem3  44858  pm14.123b  45119  rfcnpre1  45722  rfcnpre2  45734  rfcnpre3  45736  rfcnpre4  45737  climreeq  46312  funbrafv2b  47879  dfafn5a  47880  isuspgrim0  48642  gricushgr  48665  isubgrgrim  48677  rngcsectALTV  49023  ringcsectALTV  49057  elbigo2  49315  itsclc0b  49535  itscnhlinecirc02p  49548  pm5.32dav  49555  reuxfr1dd  49568  opndisj  49664  clddisj  49665  lubeldm2d  49719  glbeldm2d  49720  sectpropdlem  49797  uppropd  49942  initopropd  50004  termopropd  50005