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  3383  reubidva  3384  rmobida  3393  reubida  3394  rabbidva  3423  rabbida  3443  reuxfr1d  3716  eqrrabd  4042  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  reuhypd  5381  xpdifid  6157  xpdifcnvepel  6158  funbrfv2b  6928  dffn5  6929  feqmptdf  6941  funcnvmpt  6981  eqfnfv2  7016  fmptco  7115  dff13  7242  riotabidva  7376  mpoeq123dva  7474  mpoeq3dva  7477  opiota  8044  fnwelem  8115  suppssr  8179  mpoxopovel  8204  mpocurryd  8253  oeeui  8576  omabs  8625  eldifsucnn  8638  qliftfun  8788  erovlem  8799  mapsnend  9021  xpcomco  9043  pw2f1olem  9057  elfi2  9362  cardval2  9965  dfac2b  10102  cflim3  10234  iundom2g  10512  fpwwe2lem7  10610  fpwwe2lem11  10614  ltexpi  10875  ordpipq  10915  axrrecex  11136  nnunb  12491  zrevaddcl  12630  qrevaddcl  12986  icoshft  13491  fznn  13611  preduz  13669  predfz  13672  fznnfl  13886  fz1isolem  14488  pfxeq  14723  pfxsuffeqwrdeq  14725  pfxsuff1eqwrdeq  14726  2swrd2eqwrdeq  14980  eqwrds3  14988  2shfti  15107  limsupgle  15518  ello12  15557  elo12  15568  isercoll  15709  sumeq2ii  15734  fsum2dlem  15811  prodeq2ii  15955  bitsmod  16484  bitscmp  16486  pwsle  17536  imasleval  17585  acsfiel  17700  ismon2  17781  isepi2  17788  oppcsect  17825  subsubc  17900  funcpropd  17949  fullpropd  17969  fucsect  18022  setcsect  18136  pltval3  18383  grpidpropd  18710  ismgmid  18713  gsumpropd2lem  18727  mgmhmpropd  18746  issubmgm2  18751  mhmpropd  18840  issubm2  18852  subgacs  19218  eqgid  19239  eqg0subg  19258  ghmqusker  19348  pgpfi2  19667  eqgabl  19895  iscyggen2  19942  cyggenod  19945  eldprd  20067  subgdmdprd  20097  dprd2d2  20107  rngpropd  20243  ringpropd  20362  crngunit  20451  dvdsrpropd  20489  isrnghmmul  20515  issubrg3  20676  rngcsect  20712  ringcsect  20746  drngpropd  20842  sdrgacs  20873  lsslss  21051  lsspropd  21107  lmhmpropd  21163  lbspropd  21189  df2idl2crng  21383  znleval  21664  znunithash  21674  pjdm2  21821  islinds2  21923  aspval2  22008  bastop2  23112  elcls2  23192  neiptopreu  23251  maxlp  23265  restopn2  23295  iscnp3  23362  subbascn  23372  lmbr2  23377  kgencn  23674  kgencn2  23675  hauseqlcld  23764  txlm  23766  txkgen  23770  xkoptsub  23772  idqtop  23824  tgqtop  23830  qtopcld  23831  elmptrab  23945  flimopn  24093  fbflim  24094  fbflim2  24095  flimrest  24101  flffbas  24113  flftg  24114  cnflf  24120  cnflf2  24121  txflf  24124  isfcls  24127  fclsopn  24132  fclsbas  24139  fclsrest  24142  fcfnei  24153  cnfcf  24160  ptcmplem2  24171  tgphaus  24235  tsmssubm  24261  isucn2  24396  ismet2  24451  xblpnfps  24513  xblpnf  24514  blin  24539  blres  24549  elmopn2  24563  imasf1obl  24606  imasf1oxms  24607  prdsbl  24609  neibl  24619  metrest  24642  metcnp3  24658  metcnp  24659  metcnp2  24660  metcn  24661  txmetcnp  24665  txmetcn  24666  metuel2  24683  metucn  24689  ngppropd  24755  cnbl0  24891  cnblcld  24892  bl2ioo  24910  xrtgioo  24925  elcncf2  25010  cncfmet  25029  nmhmcn  25240  lmmbr  25378  lmmbr2  25379  iscfil2  25386  iscau2  25397  iscau3  25398  lmclim  25423  shft2rab  25628  sca2rab  25632  mbfeqalem1  25761  mbfmulc2lem  25767  mbfmax  25769  mbfposr  25772  mbfimaopnlem  25775  mbfaddlem  25780  mbfsup  25784  mbfinf  25785  i1fmullem  25814  i1fmulclem  25822  i1fres  25825  itg1climres  25834  mbfi1fseqlem4  25838  ibllem  25884  ellimc2  25997  ellimc3  25999  limcflf  26001  cnplimc  26007  cnlimc  26008  dvreslem  26029  dvcnp2  26040  dvmulbr  26059  dvcobr  26066  cmvth  26111  dvfsumle  26141  ply1remlem  26283  fta1glem2  26287  ofmulrt  26401  plyremlem  26426  ulm2  26506  mcubic  26970  cubic2  26971  dvdsflsumcom  27310  fsumvma  27335  fsumvma2  27336  vmasum  27338  logfaclbnd  27344  dchrelbas2  27359  dchrelbas3  27360  dchrelbas4  27365  lgsquadlem1  27502  lgsquadlem2  27503  2lgslem1a  27513  eqcuts2  27937  colopp  29000  colhp  29001  umgr2v2enb1  29785  upgriswlk  29899  wspthsnwspthsnon  30174  elwwlks2on  30219  elwwlks2  30227  elwspths2spth  30228  isclwwlknx  30296  clwwlkn1  30301  clwwlkn2  30304  eupth2lems  30498  fusgr2wsp2nb  30594  numclwwlkqhash  30635  isblo2  31044  ubthlem1  31131  h2hlm  31241  pjpreeq  31659  elnlfn  32189  rmounid  32751  nfpconfp  32889  fmptcof2  32914  fdifsupp  32942  suppiniseg  32943  ressupprn  32947  fpwrelmapffslem  32989  nndiffz1  33043  cntzun  33312  cntrval2  33404  urpropd  33463  lindfpropd  33611  quslsm  33630  opprqus0g  33689  ressply1mon1p  33775  ply1degltel  33801  ply1degleel  33802  algextdeglem6  34029  smatrcl  34103  zarcls  34181  rhmpreimacnlem  34191  ismntop  34333  itgeq12dv  34633  eulerpartlemgvv  34683  orvcgteel  34775  reprinrn  34922  reprdifc  34931  dfrdg2  36156  broutsideof3  36489  isfne4b  36714  filnetlem4  36754  bj-elid6  37674  bj-imdirval3  37688  nlpineqsn  37914  uncf  38110  poimirlem23  38154  poimirlem26  38157  poimirlem27  38158  heicant  38166  cnambfre  38179  itg2gt0cn  38186  ftc1anclem5  38208  areacirclem5  38223  isdrngo3  38470  isidlc  38526  erimeq2  39274  prter3  39518  islshpsm  39616  islshpat  39653  lkrsc  39733  lfl1dim  39757  ldual1dim  39802  isat3  39943  glbconxN  40014  islln2  40147  islpln2  40172  islvol2  40216  cdlemg2cex  41227  diaglbN  41691  diblsmopel  41807  dihopelvalcpre  41884  xihopellsmN  41890  dihopellsm  41891  dihglbcpreN  41936  mapdval4N  42268  hdmapoc  42567  eluzp1  42928  fsuppind  43184  fsuppssindlem2  43186  prjspreln0  43203  ellz1  43360  rmydioph  43603  rmxdioph  43605  expdiophlem1  43610  expdioph  43612  pw2f1ocnv  43626  dnwech  43637  ordeldif  43847  ordeldifsucon  43848  ordeldif1o  43849  cantnfresb  43913  tfsconcat0i  43934  tfsconcatrev  43937  oadif1lem  43968  oadif1  43969  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  rfovcnvf1od  44592  k0004lem3  44737  pm14.123b  45000  rfcnpre1  45597  rfcnpre2  45609  rfcnpre3  45611  rfcnpre4  45612  climreeq  46187  funbrafv2b  47751  dfafn5a  47752  isuspgrim0  48514  gricushgr  48537  isubgrgrim  48549  rngcsectALTV  48895  ringcsectALTV  48929  elbigo2  49183  itsclc0b  49403  itscnhlinecirc02p  49416  pm5.32dav  49423  reuxfr1dd  49436  opndisj  49532  clddisj  49533  lubeldm2d  49587  glbeldm2d  49588  sectpropdlem  49665  uppropd  49810  initopropd  49872  termopropd  49873