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  3184  rexbida  3274  rmobidva  3378  reubidva  3379  rmobida  3388  reubida  3389  rabbidva  3418  rabbida  3437  reuxfr1d  3707  eqrrabd  4011  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  reuhypd  5380  xpdifid  6158  xpdifcnvepel  6159  funbrfv2b  6942  dffn5  6943  feqmptdf  6955  funcnvmpt  6995  eqfnfv2  7030  fmptco  7130  dff13  7258  riotabidva  7396  mpoeq123dva  7494  mpoeq3dva  7497  opiota  8070  fnwelem  8145  suppssr  8215  mpoxopovel  8240  mpocurryd  8289  oeeui  8614  omabs  8663  eldifsucnn  8676  qliftfun  8826  erovlem  8837  uncf  8894  mapsnend  9067  xpcomco  9089  pw2f1olem  9103  elfi2  9409  cardval2  10075  dfac2b  10212  cflim3  10343  iundom2g  10627  fpwwe2lem7  10725  fpwwe2lem11  10729  ltexpi  10990  ordpipq  11030  axrrecex  11251  nnunb  12605  zrevaddcl  12744  qrevaddcl  13102  icoshft  13607  fznn  13729  preduz  13787  predfz  13790  fznnfl  14005  fz1isolem  14609  pfxeq  14849  pfxsuffeqwrdeq  14851  pfxsuff1eqwrdeq  14852  2swrd2eqwrdeq  15111  eqwrds3  15119  2shfti  15238  limsupgle  15649  ello12  15688  elo12  15699  isercoll  15840  sumeq2ii  15865  fsum2dlem  15941  prodeq2ii  16085  bitsmod  16611  bitscmp  16613  pwsle  17669  imasleval  17718  acsfiel  17833  ismon2  17914  isepi2  17921  oppcsect  17958  subsubc  18033  funcpropd  18082  fullpropd  18102  fucsect  18155  setcsect  18269  pltval3  18516  grpidpropd  18847  ismgmid  18850  gsumpropd2lem  18873  mgmhmpropd  18892  issubmgm2  18897  mhmpropd  18992  issubm2  19004  subgacs  19376  eqgid  19397  eqg0subg  19416  ghmqusker  19506  pgpfi2  19825  eqgabl  20053  iscyggen2  20100  cyggenod  20103  eldprd  20225  subgdmdprd  20255  dprd2d2  20265  rngpropd  20401  ringpropd  20524  crngunit  20613  dvdsrpropd  20651  isrnghmmul  20677  issubrg3  20857  rngcsect  20893  ringcsect  20927  drngpropd  21032  sdrgacs  21063  lsslss  21241  lsspropd  21297  lmhmpropd  21353  lbspropd  21379  df2idl2crng  21582  znleval  21865  znunithash  21875  pjdm2  22022  islinds2  22124  aspval2  22211  bastop2  23317  elcls2  23397  neiptopreu  23456  maxlp  23470  restopn2  23500  iscnp3  23567  subbascn  23577  lmbr2  23582  kgencn  23880  kgencn2  23881  hauseqlcld  23970  txlm  23972  txkgen  23976  xkoptsub  23978  idqtop  24030  tgqtop  24036  qtopcld  24037  elmptrab  24151  flimopn  24299  fbflim  24300  fbflim2  24301  flimrest  24307  flffbas  24319  flftg  24320  cnflf  24326  cnflf2  24327  txflf  24330  isfcls  24333  fclsopn  24338  fclsbas  24345  fclsrest  24348  fcfnei  24359  cnfcf  24366  ptcmplem2  24377  tgphaus  24441  tsmssubm  24467  isucn2  24602  ismet2  24657  xblpnfps  24719  xblpnf  24720  blin  24745  blres  24755  elmopn2  24769  imasf1obl  24812  imasf1oxms  24813  prdsbl  24815  neibl  24825  metrest  24848  metcnp3  24864  metcnp  24865  metcnp2  24866  metcn  24867  txmetcnp  24871  txmetcn  24872  metuel2  24889  metucn  24895  ngppropd  24961  cnbl0  25097  cnblcld  25098  bl2ioo  25116  xrtgioo  25131  elcncf2  25216  cncfmet  25235  nmhmcn  25446  lmmbr  25584  lmmbr2  25585  iscfil2  25592  iscau2  25603  iscau3  25604  lmclim  25629  shft2rab  25834  sca2rab  25838  mbfeqalem1  25967  mbfmulc2lem  25973  mbfmax  25975  mbfposr  25978  mbfimaopnlem  25981  mbfaddlem  25986  mbfsup  25990  mbfinf  25991  i1fmullem  26020  i1fmulclem  26028  i1fres  26031  itg1climres  26040  mbfi1fseqlem4  26044  ibllem  26090  ellimc2  26202  ellimc3  26204  limcflf  26206  cnplimc  26212  cnlimc  26213  dvreslem  26234  dvcnp2  26245  dvmulbr  26264  dvcobr  26271  cmvth  26316  dvfsumle  26346  ply1remlem  26488  fta1glem2  26492  ofmulrt  26605  plyremlem  26630  rnplynfin  26635  ulm2  26717  mcubic  27180  cubic2  27181  dvdsflsumcom  27520  fsumvma  27545  fsumvma2  27546  vmasum  27548  logfaclbnd  27554  dchrelbas2  27569  dchrelbas3  27570  dchrelbas4  27575  lgsquadlem1  27712  lgsquadlem2  27713  2lgslem1a  27723  eqcuts2  28177  colopp  29252  colhp  29253  angmgmaddcpbl  29395  dfprlng2  29430  umgr2v2enb1  30112  upgriswlk  30226  wspthsnwspthsnon  30510  elwwlks2on  30555  elwwlks2  30563  elwspths2spth  30564  isclwwlknx  30632  clwwlkn1  30637  clwwlkn2  30640  eupth2lems  30844  fusgr2wsp2nb  30940  numclwwlkqhash  30981  isblo2  31390  ubthlem1  31477  h2hlm  31587  pjpreeq  32005  elnlfn  32535  rmounid  33138  nfpconfp  33273  fmptcof2  33298  fdifsupp  33325  suppiniseg  33326  ressupprn  33330  fpwrelmapffslem  33370  nndiffz1  33424  cntzun  33686  cntrval2  33778  urpropd  33837  lindfpropd  33983  quslsm  34002  opprqus0g  34060  ressply1mon1p  34146  ply1degltel  34172  ply1degleel  34173  algextdeglem6  34400  smatrcl  34474  zarcls  34552  rhmpreimacnlem  34562  ismntop  34704  itgeq12dv  35004  eulerpartlemgvv  35054  orvcgteel  35146  reprinrn  35293  reprdifc  35302  fwfffunres  35764  dfrdg2  36649  broutsideof3  36983  isfne4b  37221  filnetlem4  37261  bj-elid6  38184  bj-imdirval3  38198  nlpineqsn  38424  poimirlem23  38654  poimirlem26  38657  poimirlem27  38658  heicant  38666  cnambfre  38679  itg2gt0cn  38686  ftc1anclem5  38708  areacirclem5  38723  isdrngo3  38986  isidlc  39042  erimeq2  39788  prter3  40032  islshpsm  40130  islshpat  40167  lkrsc  40247  lfl1dim  40271  ldual1dim  40316  isat3  40457  glbconxN  40528  islln2  40661  islpln2  40686  islvol2  40730  cdlemg2cex  41741  diaglbN  42205  diblsmopel  42321  dihopelvalcpre  42398  xihopellsmN  42404  dihopellsm  42405  dihglbcpreN  42450  mapdval4N  42782  hdmapoc  43081  eluzp1  43457  fsuppind  43711  fsuppssindlem2  43713  prjspreln0  43730  ellz1  43871  rmydioph  44114  rmxdioph  44116  expdiophlem1  44121  expdioph  44123  pw2f1ocnv  44137  dnwech  44148  ordeldif  44353  ordeldifsucon  44354  ordeldif1o  44355  cantnfresb  44419  tfsconcat0i  44440  tfsconcatrev  44443  oadif1lem  44474  oadif1  44475  fzunt  44549  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  rfovcnvf1od  45097  k0004lem3  45242  pm14.123b  45503  rfcnpre1  46129  rfcnpre2  46141  rfcnpre3  46143  rfcnpre4  46144  climreeq  46718  funbrafv2b  48322  dfafn5a  48323  isuspgrim0  49085  gricushgr  49108  isubgrgrim  49120  rngcsectALTV  49465  ringcsectALTV  49499  elbigo2  49757  itsclc0b  49977  itscnhlinecirc02p  49990  pm5.32rda  49997  reuxfr1dd  50010  opndisj  50110  clddisj  50111  lubeldm2d  50165  glbeldm2d  50166  sectpropdlem  50243  uppropd  50390  initopropd  50458  termopropd  50459  fucoisfunc2lem2  50582