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  3155  rexbida  3249  cbvrexdva2OLD  3323  rmobidva  3369  reubidva  3370  rmobida  3379  reubida  3380  rabbidva  3412  rabbida  3432  reuxfr1d  3721  eqrrabd  4049  mpteq12da  5190  mpteq12f  5192  mpteq12dva  5193  reuhypd  5374  xpdifid  6141  funbrfv2b  6918  dffn5  6919  feqmptdf  6931  eqfnfv2  7004  fmptco  7101  dff13  7229  riotabidva  7363  mpoeq123dva  7463  mpoeq3dva  7466  opiota  8038  fnwelem  8110  suppssr  8174  mpoxopovel  8199  mpocurryd  8248  oeeui  8566  omabs  8615  eldifsucnn  8628  qliftfun  8775  erovlem  8786  mapsnend  9007  xpcomco  9031  pw2f1olem  9045  elfi2  9365  cardval2  9944  dfac2b  10084  cflim3  10215  iundom2g  10493  fpwwe2lem7  10590  fpwwe2lem11  10594  ltexpi  10855  ordpipq  10895  axrrecex  11116  nnunb  12438  zrevaddcl  12578  qrevaddcl  12930  icoshft  13434  fznn  13553  preduz  13611  predfz  13614  fznnfl  13824  fz1isolem  14426  pfxeq  14661  pfxsuffeqwrdeq  14663  pfxsuff1eqwrdeq  14664  2swrd2eqwrdeq  14919  eqwrds3  14927  2shfti  15046  limsupgle  15443  ello12  15482  elo12  15493  isercoll  15634  sumeq2ii  15659  fsum2dlem  15736  prodeq2ii  15877  bitsmod  16406  bitscmp  16408  pwsle  17455  imasleval  17504  acsfiel  17615  ismon2  17696  isepi2  17703  oppcsect  17740  subsubc  17815  funcpropd  17864  fullpropd  17884  fucsect  17937  setcsect  18051  pltval3  18298  grpidpropd  18589  ismgmid  18592  gsumpropd2lem  18606  mgmhmpropd  18625  issubmgm2  18630  mhmpropd  18719  issubm2  18731  subgacs  19093  eqgid  19112  eqg0subg  19128  ghmqusker  19219  pgpfi2  19536  eqgabl  19764  iscyggen2  19811  cyggenod  19814  eldprd  19936  subgdmdprd  19966  dprd2d2  19976  rngpropd  20083  ringpropd  20197  crngunit  20287  dvdsrpropd  20325  isrnghmmul  20351  issubrg3  20509  rngcsect  20545  ringcsect  20579  drngpropd  20678  sdrgacs  20710  lsslss  20867  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  znleval  21464  znunithash  21474  pjdm2  21620  islinds2  21722  aspval2  21807  bastop2  22881  elcls2  22961  neiptopreu  23020  maxlp  23034  restopn2  23064  iscnp3  23131  subbascn  23141  lmbr2  23146  kgencn  23443  kgencn2  23444  hauseqlcld  23533  txlm  23535  txkgen  23539  xkoptsub  23541  idqtop  23593  tgqtop  23599  qtopcld  23600  elmptrab  23714  flimopn  23862  fbflim  23863  fbflim2  23864  flimrest  23870  flffbas  23882  flftg  23883  cnflf  23889  cnflf2  23890  txflf  23893  isfcls  23896  fclsopn  23901  fclsbas  23908  fclsrest  23911  fcfnei  23922  cnfcf  23929  ptcmplem2  23940  tgphaus  24004  tsmssubm  24030  isucn2  24166  ismet2  24221  xblpnfps  24283  xblpnf  24284  blin  24309  blres  24319  elmopn2  24333  imasf1obl  24376  imasf1oxms  24377  prdsbl  24379  neibl  24389  metrest  24412  metcnp3  24428  metcnp  24429  metcnp2  24430  metcn  24431  txmetcnp  24435  txmetcn  24436  metuel2  24453  metucn  24459  ngppropd  24525  cnbl0  24661  cnblcld  24662  bl2ioo  24680  xrtgioo  24695  elcncf2  24783  cncfmet  24802  nmhmcn  25020  lmmbr  25158  lmmbr2  25159  iscfil2  25166  iscau2  25177  iscau3  25178  lmclim  25203  shft2rab  25409  sca2rab  25413  mbfeqalem1  25542  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  mbfimaopnlem  25556  mbfaddlem  25561  mbfsup  25565  mbfinf  25566  i1fmullem  25595  i1fmulclem  25603  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  ibllem  25665  ellimc2  25778  ellimc3  25780  limcflf  25782  cnplimc  25788  cnlimc  25789  dvreslem  25810  dvcnp2  25821  dvmulbr  25841  dvcobr  25849  cmvth  25895  dvfsumle  25926  ply1remlem  26070  fta1glem2  26074  ofmulrt  26189  plyremlem  26212  ulm2  26294  mcubic  26757  cubic2  26758  dvdsflsumcom  27098  fsumvma  27124  fsumvma2  27125  vmasum  27127  logfaclbnd  27133  dchrelbas2  27148  dchrelbas3  27149  dchrelbas4  27154  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a  27302  eqscut2  27718  colopp  28696  colhp  28697  umgr2v2enb1  29454  upgriswlk  29569  wspthsnwspthsnon  29846  elwwlks2on  29889  elwwlks2  29896  elwspths2spth  29897  isclwwlknx  29965  clwwlkn1  29970  clwwlkn2  29973  eupth2lems  30167  fusgr2wsp2nb  30263  numclwwlkqhash  30304  isblo2  30712  ubthlem1  30799  h2hlm  30909  pjpreeq  31327  elnlfn  31857  rmounid  32424  nfpconfp  32556  fmptcof2  32581  funcnvmpt  32591  fdifsupp  32608  suppiniseg  32609  ressupprn  32613  fpwrelmapffslem  32655  nndiffz1  32709  cntzun  33008  cntrval2  33128  urpropd  33183  lindfpropd  33353  quslsm  33376  opprqus0g  33461  ressply1mon1p  33537  ply1degltel  33560  ply1degleel  33561  algextdeglem6  33712  smatrcl  33786  zarcls  33864  rhmpreimacnlem  33874  ismntop  34016  itgeq12dv  34317  eulerpartlemgvv  34367  orvcgteel  34459  reprinrn  34609  reprdifc  34618  dfrdg2  35783  broutsideof3  36114  isfne4b  36329  filnetlem4  36369  bj-elid6  37158  bj-imdirval3  37172  nlpineqsn  37396  uncf  37593  poimirlem23  37637  poimirlem26  37640  poimirlem27  37641  heicant  37649  cnambfre  37662  itg2gt0cn  37669  ftc1anclem5  37691  areacirclem5  37706  isdrngo3  37953  isidlc  38009  erimeq2  38670  prter3  38875  islshpsm  38973  islshpat  39010  lkrsc  39090  lfl1dim  39114  ldual1dim  39159  isat3  39300  glbconxN  39372  islln2  39505  islpln2  39530  islvol2  39574  cdlemg2cex  40585  diaglbN  41049  diblsmopel  41165  dihopelvalcpre  41242  xihopellsmN  41248  dihopellsm  41249  dihglbcpreN  41294  mapdval4N  41626  hdmapoc  41925  eluzp1  42295  fsuppind  42578  fsuppssindlem2  42580  prjspreln0  42597  ellz1  42755  rmydioph  43003  rmxdioph  43005  expdiophlem1  43010  expdioph  43012  pw2f1ocnv  43026  dnwech  43037  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  44415  rfcnpre1  45013  rfcnpre2  45025  rfcnpre3  45027  rfcnpre4  45028  climreeq  45611  funbrafv2b  47160  dfafn5a  47161  isuspgrim0  47894  gricushgr  47917  isubgrgrim  47929  rngcsectALTV  48263  ringcsectALTV  48297  elbigo2  48541  itsclc0b  48761  itscnhlinecirc02p  48774  pm5.32dav  48782  reuxfr1dd  48795  opndisj  48891  clddisj  48892  lubeldm2d  48946  glbeldm2d  48947  sectpropdlem  49025  uppropd  49170  initopropd  49232  termopropd  49233