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  3188  rexbida  3278  rmobidva  3382  reubidva  3383  rmobida  3392  reubida  3393  rabbidva  3422  rabbida  3441  reuxfr1d  3711  eqrrabd  4014  mpteq12da  5192  mpteq12f  5194  mpteq12dva  5195  reuhypd  5386  xpdifid  6172  xpdifcnvepel  6173  funbrfv2b  6968  dffn5  6969  feqmptdf  6981  funcnvmpt  7021  eqfnfv2  7056  elpreima  7083  fmptco  7157  dff13  7284  riotabidva  7422  mpoeq123dva  7520  mpoeq3dva  7523  opiota  8098  fnwelem  8173  suppssr  8243  mpoxopovel  8268  mpocurryd  8317  oeeui  8642  omabs  8691  eldifsucnn  8704  qliftfun  8854  erovlem  8865  uncf  8922  mapsnend  9095  xpcomco  9117  pw2f1olem  9131  elfi2  9436  cardval2  10102  dfac2b  10239  cflim3  10370  iundom2g  10654  fpwwe2lem7  10752  fpwwe2lem11  10756  ltexpi  11017  ordpipq  11057  axrrecex  11278  nnunb  12632  zrevaddcl  12771  qrevaddcl  13129  icoshft  13634  fznn  13756  preduz  13814  predfz  13817  fznnfl  14032  fz1isolem  14636  pfxeq  14876  pfxsuffeqwrdeq  14878  pfxsuff1eqwrdeq  14879  2swrd2eqwrdeq  15138  eqwrds3  15146  2shfti  15265  limsupgle  15676  ello12  15715  elo12  15726  isercoll  15867  sumeq2ii  15892  fsum2dlem  15968  prodeq2ii  16112  bitsmod  16638  bitscmp  16640  pwsle  17696  imasleval  17745  acsfiel  17860  ismon2  17941  isepi2  17948  oppcsect  17985  subsubc  18060  funcpropd  18109  fullpropd  18129  fucsect  18182  setcsect  18296  pltval3  18543  grpidpropd  18874  ismgmid  18877  gsumpropd2lem  18900  mgmhmpropd  18919  issubmgm2  18924  mhmpropd  19019  issubm2  19031  subgacs  19403  eqgid  19424  eqg0subg  19443  ghmqusker  19534  pgpfi2  19853  eqgabl  20081  iscyggen2  20128  cyggenod  20131  eldprd  20253  subgdmdprd  20283  dprd2d2  20293  rngpropd  20429  ringpropd  20552  crngunit  20641  dvdsrpropd  20679  isrnghmmul  20705  issubrg3  20885  rngcsect  20921  ringcsect  20955  drngpropd  21060  sdrgacs  21091  lsslss  21269  lsspropd  21325  lmhmpropd  21381  lbspropd  21407  df2idl2crng  21610  znleval  21893  znunithash  21903  pjdm2  22050  islinds2  22152  aspval2  22239  bastop2  23345  elcls2  23425  neiptopreu  23484  maxlp  23498  restopn2  23528  iscnp3  23595  subbascn  23605  lmbr2  23610  kgencn  23908  kgencn2  23909  hauseqlcld  23998  txlm  24000  txkgen  24004  xkoptsub  24006  idqtop  24058  tgqtop  24064  qtopcld  24065  elmptrab  24179  flimopn  24327  fbflim  24328  fbflim2  24329  flimrest  24335  flffbas  24347  flftg  24348  cnflf  24354  cnflf2  24355  txflf  24358  isfcls  24361  fclsopn  24366  fclsbas  24373  fclsrest  24376  fcfnei  24387  cnfcf  24394  ptcmplem2  24405  tgphaus  24469  tsmssubm  24495  isucn2  24630  ismet2  24685  xblpnfps  24747  xblpnf  24748  blin  24773  blres  24783  elmopn2  24797  imasf1obl  24840  imasf1oxms  24841  prdsbl  24843  neibl  24853  metrest  24876  metcnp3  24892  metcnp  24893  metcnp2  24894  metcn  24895  txmetcnp  24899  txmetcn  24900  metuel2  24917  metucn  24923  ngppropd  24989  cnbl0  25125  cnblcld  25126  bl2ioo  25144  xrtgioo  25159  elcncf2  25244  cncfmet  25263  nmhmcn  25474  lmmbr  25612  lmmbr2  25613  iscfil2  25620  iscau2  25631  iscau3  25632  lmclim  25657  shft2rab  25862  sca2rab  25866  mbfeqalem1  25995  mbfmulc2lem  26001  mbfmax  26003  mbfposr  26006  mbfimaopnlem  26009  mbfaddlem  26014  mbfsup  26018  mbfinf  26019  i1fmullem  26048  i1fmulclem  26056  i1fres  26059  itg1climres  26068  mbfi1fseqlem4  26072  ibllem  26118  ellimc2  26230  ellimc3  26232  limcflf  26234  cnplimc  26240  cnlimc  26241  dvreslem  26262  dvcnp2  26273  dvmulbr  26292  dvcobr  26299  cmvth  26344  dvfsumle  26374  ply1remlem  26516  fta1glem2  26520  ofmulrt  26633  plyremlem  26658  rnplynfin  26663  ulm2  26745  mcubic  27208  cubic2  27209  dvdsflsumcom  27548  fsumvma  27573  fsumvma2  27574  vmasum  27576  logfaclbnd  27582  dchrelbas2  27597  dchrelbas3  27598  dchrelbas4  27603  lgsquadlem1  27740  lgsquadlem2  27741  2lgslem1a  27751  eqcuts2  28205  colopp  29280  colhp  29281  angmgmaddcpbl  29423  dfprlng2  29458  umgr2v2enb1  30140  upgriswlk  30254  wspthsnwspthsnon  30538  elwwlks2on  30583  elwwlks2  30591  elwspths2spth  30592  isclwwlknx  30660  clwwlkn1  30665  clwwlkn2  30668  eupth2lems  30872  fusgr2wsp2nb  30968  numclwwlkqhash  31009  isblo2  31418  ubthlem1  31505  h2hlm  31615  pjpreeq  32033  elnlfn  32563  rmounid  33166  nfpconfp  33301  fmptcof2  33326  fdifsupp  33352  suppiniseg  33353  ressupprn  33357  fpwrelmapffslem  33397  nndiffz1  33451  cntzun  33716  cntrval2  33808  urpropd  33867  lindfpropd  34021  quslsm  34040  opprqus0g  34098  ressply1mon1p  34183  ply1degltel  34209  ply1degleel  34210  algextdeglem6  34437  smatrcl  34511  zarcls  34589  rhmpreimacnlem  34599  ismntop  34741  itgeq12dv  35041  eulerpartlemgvv  35091  orvcgteel  35183  reprinrn  35330  reprdifc  35339  fwfffunres  35801  dfrdg2  36748  broutsideof3  37082  isfne4b  37320  filnetlem4  37360  bj-elid6  38296  bj-imdirval3  38310  nlpineqsn  38536  poimirlem23  38766  poimirlem26  38769  poimirlem27  38770  heicant  38778  cnambfre  38791  itg2gt0cn  38798  ftc1anclem5  38820  areacirclem5  38835  isdrngo3  39096  isidlc  39152  erimeq2  39898  prter3  40142  islshpsm  40240  islshpat  40277  lkrsc  40357  lfl1dim  40381  ldual1dim  40426  isat3  40567  glbconxN  40638  islln2  40771  islpln2  40796  islvol2  40840  cdlemg2cex  41851  diaglbN  42315  diblsmopel  42431  dihopelvalcpre  42508  xihopellsmN  42514  dihopellsm  42515  dihglbcpreN  42560  mapdval4N  42892  hdmapoc  43191  eluzp1  43568  fsuppind  43822  fsuppssindlem2  43824  prjspreln0  43841  ellz1  43982  rmydioph  44225  rmxdioph  44227  expdiophlem1  44232  expdioph  44234  pw2f1ocnv  44248  dnwech  44259  ordeldif  44463  ordeldifsucon  44464  ordeldif1o  44465  cantnfresb  44529  tfsconcat0i  44550  tfsconcatrev  44553  oadif1lem  44584  oadif1  44585  fzunt  44659  fzuntd  44660  fzunt1d  44661  fzuntgd  44662  rfovcnvf1od  45207  k0004lem3  45352  pm14.123b  45612  rfcnpre1  46252  rfcnpre2  46264  rfcnpre3  46266  rfcnpre4  46267  climreeq  46840  funbrafv2b  48444  dfafn5a  48445  isuspgrim0  49207  gricushgr  49230  isubgrgrim  49242  rngcsectALTV  49587  ringcsectALTV  49621  elbigo2  49879  itsclc0b  50099  itscnhlinecirc02p  50112  pm5.32rda  50119  reuxfr1dd  50132  opndisj  50232  clddisj  50233  lubeldm2d  50287  glbeldm2d  50288  sectpropdlem  50365  uppropd  50512  initopropd  50580  termopropd  50581  fucoisfunc2lem2  50704